1  /-
  2  Copyright (c) 2017 Mario Carneiro. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Authors: Mario Carneiro, Johannes Hölzl
  5  
  6  Ordered monoids and groups.
  7  -/
  8  import algebra.group order.bounded_lattice tactic.basic
src         └───────────┘ └───────────────────┘ └──────────┘
  9  
 10  universe u
 11  variable {α : Type u}
 12  
 13  section old_structure_cmd
 14  
 15  set_option old_structure_cmd true
doc             └───────────────┘
 16  set_option default_priority 100 -- see Note [default priority]
doc             └──────────────┘
 17  /-- An ordered (additive) commutative monoid is a commutative monoid
 18    with a partial order such that addition is an order embedding, i.e.
 19    `a + b ≤ a + c ↔ b ≤ c`. These monoids are automatically cancellative. -/
 20  class ordered_comm_monoid (α : Type*) extends add_comm_monoid α, partial_order α :=
id                                 └───┘          └─────────────┘   └───────────┘ 
src                                                └─────────────┘    └───────────┘
typ                                └───┘          └─────────────┘   └───────────┘ 
 21  (add_le_add_left       : ∀ a b : α, a ≤ b → ∀ c : α, c + a ≤ c + b)
id                                                        
src                                                             
typ                                                       
 22  (lt_of_add_lt_add_left : ∀ a b c : α, a + b < a + c → b < c)
id                                                  
src                                                      
typ                                                 
 23  
 24  /-- A canonically ordered monoid is an ordered commutative monoid
 25    in which the ordering coincides with the divisibility relation,
 26    which is to say, `a ≤ b` iff there exists `c` with `b = a + c`.
 27    This is satisfied by the natural numbers, for example, but not
 28    the integers or other ordered groups. -/
 29  class canonically_ordered_monoid (α : Type*) extends ordered_comm_monoid α, lattice.order_bot α :=
id                                        └───┘          └─────────────────┘   └───────────────┘ 
src                                                       └─────────────────┘    └───────────────┘
typ                                       └───┘          └─────────────────┘   └───────────────┘ 
doc                                                       └─────────────────┘    └───────────────┘
 30  (le_iff_exists_add : ∀a b:α, a ≤ b ↔ ∃c, b = a + c)
id                                       
src                                            
typ                                      
 31  
 32  end old_structure_cmd
 33  
 34  section ordered_comm_monoid
 35  variables [ordered_comm_monoid α] {a b c d : α}
id              └─────────────────┘
src             └─────────────────┘
typ             └─────────────────┘
doc             └─────────────────┘
 36  
 37  lemma add_le_add_left' (h : a ≤ b) : c + a ≤ c + b :=
id                                           
src                                              
typ                                          
 38  ordered_comm_monoid.add_le_add_left a b h c
id   └─────────────────────────────────┘    
src  └─────────────────────────────────┘
typ  └─────────────────────────────────┘    
 39  
 40  lemma add_le_add_right' (h : a ≤ b) : a + c ≤ b + c :=
id                                            
src                                               
typ                                           
 41  add_comm c a ▸ add_comm c b ▸ add_le_add_left' h
id   └──────┘    └──────┘    └──────────────┘ 
src  └──────┘      └──────┘      └──────────────┘
typ  └──────┘    └──────┘    └──────────────┘ 
 42  
 43  lemma lt_of_add_lt_add_left' : a + b < a + c → b < c :=
id                                             
src                                                
typ                                            
 44  ordered_comm_monoid.lt_of_add_lt_add_left a b c
id   └───────────────────────────────────────┘   
src  └───────────────────────────────────────┘
typ  └───────────────────────────────────────┘   
 45  
 46  lemma add_le_add' (h₁ : a ≤ b) (h₂ : c ≤ d) : a + c ≤ b + d :=
id                                                 
src                                                      
typ                                                
 47  le_trans (add_le_add_right' h₁) (add_le_add_left' h₂)
id   └──────┘  └───────────────┘ └┘   └──────────────┘ └┘
src  └──────┘  └───────────────┘      └──────────────┘
typ  └──────┘  └───────────────┘ └┘   └──────────────┘ └┘
 48  
 49  lemma le_add_of_nonneg_right' (h : 0 ≤ b) : a ≤ a + b :=
id                                                 
src                                                  
typ                                                
 50  have a + b ≥ a + 0, from add_le_add_left' h,
id                      └──────────────┘ 
src                        └──────────────┘
typ                     └──────────────┘ 
 51  by rwa add_zero at this
id          └──────┘
src     └──┘└──────┘└────────
typ     └──┘└──────┘└────────
doc     └──┘        └────────
txt     └──┘        └────────
par     └──┘        └────────
pid                └──────┘
st     └─────────────────────
 52  
src  
typ  
doc  
txt  
par  
pid  
st   
 53  lemma le_add_of_nonneg_left' (h : 0 ≤ b) : a ≤ b + a :=
id                                                
src                                                 
typ                                               
 54  have 0 + a ≤ b + a, from add_le_add_right' h,
id                      └───────────────┘ 
src                        └───────────────┘
typ                     └───────────────┘ 
 55  by rwa zero_add at this
id          └──────┘
src     └──┘└──────┘└────────
typ     └──┘└──────┘└────────
doc     └──┘        └────────
txt     └──┘        └────────
par     └──┘        └────────
pid                └──────┘
st     └─────────────────────
 56  
src  
typ  
doc  
txt  
par  
pid  
st   
 57  lemma lt_of_add_lt_add_right' (h : a + b < c + b) : a < c :=
id                                                  
src                                                     
typ                                                 
 58  lt_of_add_lt_add_left'
id   └────────────────────┘
src  └────────────────────┘
typ  └────────────────────┘
 59    (show b + a < b + c, begin rw [add_comm b a, add_comm b c], assumption end)
id                             └──────┘    └──────┘  
src                            └──┘└──────┘  └┘└──────┘    └─────────┘
typ                        └──┘└──────┘└┘└──────┘  └─────────┘
doc                               └──┘          └┘            └─────────┘
txt                               └──┘          └┘            └─────────┘
par                               └──┘          └┘            └─────────┘
pid                                 └┘          └┘                      
st                          └────────────────────┘└────────────┘└────────────┘└─┘
 60  
 61  -- here we start using properties of zero.
 62  lemma le_add_of_nonneg_of_le' (ha : 0 ≤ a) (hbc : b ≤ c) : b ≤ a + c :=
id                                                             
src                                                                
typ                                                            
 63  zero_add b ▸ add_le_add' ha hbc
id   └──────┘   └─────────┘ └┘ └─┘
src  └──────┘    └─────────┘
typ  └──────┘   └─────────┘ └┘ └─┘
 64  
 65  lemma le_add_of_le_of_nonneg' (hbc : b ≤ c) (ha : 0 ≤ a) : b ≤ c + a :=
id                                                             
src                                                                
typ                                                            
 66  add_zero b ▸ add_le_add' hbc ha
id   └──────┘   └─────────┘ └─┘ └┘
src  └──────┘    └─────────┘
typ  └──────┘   └─────────┘ └─┘ └┘
 67  
 68  lemma add_nonneg' (ha : 0 ≤ a) (hb : 0 ≤ b) : 0 ≤ a + b :=
id                                                  
src                                                   
typ                                                 
 69  le_add_of_nonneg_of_le' ha hb
id   └─────────────────────┘ └┘ └┘
src  └─────────────────────┘
typ  └─────────────────────┘ └┘ └┘
 70  
 71  lemma add_pos_of_pos_of_nonneg' (ha : 0 < a) (hb : 0 ≤ b) : 0 < a + b :=
id                                                                
src                                                                 
typ                                                               
 72  lt_of_lt_of_le ha $ le_add_of_nonneg_right' hb
id   └────────────┘ └┘   └─────────────────────┘ └┘
src  └────────────┘      └─────────────────────┘
typ  └────────────┘ └┘   └─────────────────────┘ └┘
 73  
 74  lemma add_pos' (ha : 0 < a) (hb : 0 < b) : 0 < a + b :=
id                                               
src                                                
typ                                              
 75  add_pos_of_pos_of_nonneg' ha $ le_of_lt hb
id   └───────────────────────┘ └┘   └──────┘ └┘
src  └───────────────────────┘      └──────┘
typ  └───────────────────────┘ └┘   └──────┘ └┘
 76  
 77  lemma add_pos_of_nonneg_of_pos' (ha : 0 ≤ a) (hb : 0 < b) : 0 < a + b :=
id                                                                
src                                                                 
typ                                                               
 78  lt_of_lt_of_le hb $ le_add_of_nonneg_left' ha
id   └────────────┘ └┘   └────────────────────┘ └┘
src  └────────────┘      └────────────────────┘
typ  └────────────┘ └┘   └────────────────────┘ └┘
 79  
 80  lemma add_nonpos' (ha : a ≤ 0) (hb : b ≤ 0) : a + b ≤ 0 :=
id                                                
src                                                   
typ                                               
 81  zero_add (0:α) ▸ (add_le_add' ha hb)
id   └──────┘        └─────────┘ └┘ └┘
src  └──────┘         └─────────┘
typ  └──────┘        └─────────┘ └┘ └┘
 82  
 83  lemma add_le_of_nonpos_of_le' (ha : a ≤ 0) (hbc : b ≤ c) : a + b ≤ c :=
id                                                             
src                                                                
typ                                                            
 84  zero_add c ▸ add_le_add' ha hbc
id   └──────┘   └─────────┘ └┘ └─┘
src  └──────┘    └─────────┘
typ  └──────┘   └─────────┘ └┘ └─┘
 85  
 86  lemma add_le_of_le_of_nonpos' (hbc : b ≤ c) (ha : a ≤ 0) : b + a ≤ c :=
id                                                             
src                                                                
typ                                                            
 87  add_zero c ▸ add_le_add' hbc ha
id   └──────┘   └─────────┘ └─┘ └┘
src  └──────┘    └─────────┘
typ  └──────┘   └─────────┘ └─┘ └┘
 88  
 89  lemma add_neg_of_neg_of_nonpos' (ha : a < 0) (hb : b ≤ 0) : a + b < 0 :=
id                                                              
src                                                                 
typ                                                             
 90  lt_of_le_of_lt (add_le_of_le_of_nonpos' (le_refl _) hb) ha
id   └────────────┘  └─────────────────────┘  └─────┘    └┘  └┘
src  └────────────┘  └─────────────────────┘  └─────┘
typ  └────────────┘  └─────────────────────┘  └─────┘    └┘  └┘
 91  
 92  lemma add_neg_of_nonpos_of_neg' (ha : a ≤ 0) (hb : b < 0) : a + b < 0 :=
id                                                              
src                                                                 
typ                                                             
 93  lt_of_le_of_lt (add_le_of_nonpos_of_le' ha (le_refl _)) hb
id   └────────────┘  └─────────────────────┘ └┘  └─────┘     └┘
src  └────────────┘  └─────────────────────┘     └─────┘
typ  └────────────┘  └─────────────────────┘ └┘  └─────┘     └┘
 94  
 95  lemma add_neg' (ha : a < 0) (hb : b < 0) : a + b < 0 :=
id                                             
src                                                
typ                                            
 96  add_neg_of_nonpos_of_neg' (le_of_lt ha) hb
id   └───────────────────────┘  └──────┘ └┘  └┘
src  └───────────────────────┘  └──────┘
typ  └───────────────────────┘  └──────┘ └┘  └┘
 97  
 98  lemma lt_add_of_nonneg_of_lt' (ha : 0 ≤ a) (hbc : b < c) : b < a + c :=
id                                                             
src                                                                
typ                                                            
 99  lt_of_lt_of_le hbc $ le_add_of_nonneg_left' ha
id   └────────────┘ └─┘   └────────────────────┘ └┘
src  └────────────┘       └────────────────────┘
typ  └────────────┘ └─┘   └────────────────────┘ └┘
100  
101  lemma lt_add_of_lt_of_nonneg' (hbc : b < c) (ha : 0 ≤ a) : b < c + a :=
id                                                             
src                                                                
typ                                                            
102  lt_of_lt_of_le hbc $ le_add_of_nonneg_right' ha
id   └────────────┘ └─┘   └─────────────────────┘ └┘
src  └────────────┘       └─────────────────────┘
typ  └────────────┘ └─┘   └─────────────────────┘ └┘
103  
104  lemma lt_add_of_pos_of_lt' (ha : 0 < a) (hbc : b < c) : b < a + c :=
id                                                          
src                                                             
typ                                                         
st                                  
105  lt_add_of_nonneg_of_lt' (le_of_lt ha) hbc
id   └─────────────────────┘  └──────┘ └┘  └─┘
src  └─────────────────────┘  └──────┘
typ  └─────────────────────┘  └──────┘ └┘  └─┘
106  
107  lemma lt_add_of_lt_of_pos' (hbc : b < c) (ha : 0 < a) : b < c + a :=
id                                                          
src                                                             
typ                                                         
108  lt_add_of_lt_of_nonneg' hbc (le_of_lt ha)
id   └─────────────────────┘ └─┘  └──────┘ └┘
src  └─────────────────────┘      └──────┘
typ  └─────────────────────┘ └─┘  └──────┘ └┘
109  
110  lemma add_lt_of_nonpos_of_lt' (ha : a ≤ 0) (hbc : b < c) : a + b < c :=
id                                                             
src                                                                
typ                                                            
111  lt_of_le_of_lt (add_le_of_nonpos_of_le' ha (le_refl _)) hbc
id   └────────────┘  └─────────────────────┘ └┘  └─────┘     └─┘
src  └────────────┘  └─────────────────────┘     └─────┘
typ  └────────────┘  └─────────────────────┘ └┘  └─────┘     └─┘
112  
113  lemma add_lt_of_lt_of_nonpos' (hbc : b < c) (ha : a ≤ 0)  : b + a < c :=
id                                                              
src                                                                 
typ                                                             
114  lt_of_le_of_lt (add_le_of_le_of_nonpos' (le_refl _) ha) hbc
id   └────────────┘  └─────────────────────┘  └─────┘    └┘  └─┘
src  └────────────┘  └─────────────────────┘  └─────┘
typ  └────────────┘  └─────────────────────┘  └─────┘    └┘  └─┘
115  
116  lemma add_lt_of_neg_of_lt' (ha : a < 0) (hbc : b < c) : a + b < c :=
id                                                          
src                                                             
typ                                                         
117  add_lt_of_nonpos_of_lt' (le_of_lt ha) hbc
id   └─────────────────────┘  └──────┘ └┘  └─┘
src  └─────────────────────┘  └──────┘
typ  └─────────────────────┘  └──────┘ └┘  └─┘
118  
119  lemma add_lt_of_lt_of_neg' (hbc : b < c) (ha : a < 0) : b + a < c :=
id                                                          
src                                                             
typ                                                         
120  add_lt_of_lt_of_nonpos' hbc (le_of_lt ha)
id   └─────────────────────┘ └─┘  └──────┘ └┘
src  └─────────────────────┘      └──────┘
typ  └─────────────────────┘ └─┘  └──────┘ └┘
121  
122  lemma add_eq_zero_iff' (ha : 0 ≤ a) (hb : 0 ≤ b) : a + b = 0 ↔ a = 0 ∧ b = 0 :=
id                                                               
src                                                                    
typ                                                              
123  iff.intro
id   └───────┘
src  └───────┘
typ  └───────┘
124    (assume hab : a + b = 0,
id                      
src                       
typ                     
125     have a ≤ 0, from hab ▸ le_add_of_le_of_nonneg' (le_refl _) hb,
id                     └─┘  └─────────────────────┘  └─────┘    └┘
src                          └─────────────────────┘  └─────┘
typ                    └─┘  └─────────────────────┘  └─────┘    └┘
126     have a = 0, from le_antisymm this ha,
id                     └─────────┘ └──┘ └┘
src                     └─────────┘
typ                    └─────────┘ └──┘ └┘
127     have b ≤ 0, from hab ▸ le_add_of_nonneg_of_le' ha (le_refl _),
id                     └─┘  └─────────────────────┘ └┘  └─────┘
src                          └─────────────────────┘     └─────┘
typ                    └─┘  └─────────────────────┘ └┘  └─────┘
128     have b = 0, from le_antisymm this hb,
id                     └─────────┘ └──┘ └┘
src                     └─────────┘
typ                    └─────────┘ └──┘ └┘
129     and.intro ‹a = 0› ‹b = 0›)
id      └───────┘        
src     └───────┘          
typ     └───────┘        
doc                          
130    (assume ⟨ha', hb'⟩, by rw [ha', hb', add_zero])
id                               └─┘  └─┘  └──────┘
src                           └──┘   └┘   └┘└──────┘
typ                          └──┘└─┘└┘└─┘└┘└──────┘
doc                           └──┘   └┘   └┘        
txt                           └──┘   └┘   └┘        
par                           └──┘   └┘   └┘        
pid                             └┘   └┘   └┘        
st                           └──────┘└───┘└────────┘
131  
132  lemma bit0_pos {a : α} (h : 0 < a) : 0 < bit0 a :=
id                                        └──┘ 
src                                         └──┘
typ                                       └──┘ 
133  add_pos' h h
id   └──────┘  
src  └──────┘
typ  └──────┘  
134  
135  end ordered_comm_monoid
136  
137  namespace units
138  
139  instance [monoid α] [i : preorder α] : preorder (units α) :=
id             └────┘        └──────┘     └──────┘  └───┘ 
src            └────┘         └──────┘      └──────┘  └───┘
typ            └────┘        └──────┘     └──────┘  └───┘ 
140  preorder.lift (coe : units α → α) i
id   └───────────┘  └─┘   └───┘      
src  └───────────┘  └─┘   └───┘
typ  └───────────┘  └─┘   └───┘      
141  
142  @[simp] theorem coe_le_coe [monoid α] [preorder α] {a b : units α} :
id                               └────┘    └──────┘          └───┘ 
src                              └────┘     └──────┘           └───┘
typ                              └────┘    └──────┘          └───┘ 
doc    └──┘
143    (a : α) ≤ b ↔ a ≤ b := iff.rfl
id                    └─────┘
src                        └─────┘
typ                   └─────┘
144  
145  @[simp] theorem coe_lt_coe [monoid α] [preorder α] {a b : units α} :
id                               └────┘    └──────┘          └───┘ 
src                              └────┘     └──────┘           └───┘
typ                              └────┘    └──────┘          └───┘ 
doc    └──┘
146    (a : α) < b ↔ a < b := iff.rfl
id                    └─────┘
src                        └─────┘
typ                   └─────┘
147  
148  instance [monoid α] [i : partial_order α] : partial_order (units α) :=
id             └────┘        └───────────┘     └───────────┘  └───┘ 
src            └────┘         └───────────┘      └───────────┘  └───┘
typ            └────┘        └───────────┘     └───────────┘  └───┘ 
149  partial_order.lift (coe : units α → α) (by ext) i
id   └────────────────┘  └─┘   └───┘               
src  └────────────────┘  └─┘   └───┘            └─┘
typ  └────────────────┘  └─┘   └───┘          └─┘  
doc                                             └─┘
txt                                             └─┘
par                                             └─┘
st                                             └──┘
150  
151  instance [monoid α] [i : linear_order α] : linear_order (units α) :=
id             └────┘        └──────────┘     └──────────┘  └───┘ 
src            └────┘         └──────────┘      └──────────┘  └───┘
typ            └────┘        └──────────┘     └──────────┘  └───┘ 
152  linear_order.lift (coe : units α → α) (by ext) i
id   └───────────────┘  └─┘   └───┘               
src  └───────────────┘  └─┘   └───┘            └─┘
typ  └───────────────┘  └─┘   └───┘          └─┘  
doc                                            └─┘
txt                                            └─┘
par                                            └─┘
st                                            └──┘
153  
154  instance [monoid α] [i : decidable_linear_order α] : decidable_linear_order (units α) :=
id             └────┘        └────────────────────┘     └────────────────────┘  └───┘ 
src            └────┘         └────────────────────┘      └────────────────────┘  └───┘
typ            └────┘        └────────────────────┘     └────────────────────┘  └───┘ 
155  decidable_linear_order.lift (coe : units α → α) (by ext) i
id   └─────────────────────────┘  └─┘   └───┘               
src  └─────────────────────────┘  └─┘   └───┘            └─┘
typ  └─────────────────────────┘  └─┘   └───┘          └─┘  
doc                                                      └─┘
txt                                                      └─┘
par                                                      └─┘
st                                                      └──┘
156  
157  theorem max_coe [monoid α] [decidable_linear_order α] {a b : units α} :
id                    └────┘    └────────────────────┘          └───┘ 
src                   └────┘     └────────────────────┘           └───┘
typ                   └────┘    └────────────────────┘          └───┘ 
158    (↑(max a b) : α) = max a b :=
id       └─┘         └─┘  
src      └─┘            └─┘
typ      └─┘         └─┘  
159  by by_cases a ≤ b; simp [max, h]
id                         └─┘  
src     └───────┘    └────┘└─┘└┘ └─
typ     └───────┘  └────┘└─┘└┘└─
doc     └───────┘     └────┘   └┘ └─
txt     └───────┘     └────┘   └┘ └─
par     └───────┘     └────┘   └┘ └─
pid                         └┘ 
st     └──────────────────────────────
160  
src  
typ  
doc  
txt  
par  
pid  
st   
161  theorem min_coe [monoid α] [decidable_linear_order α] {a b : units α} :
id                    └────┘    └────────────────────┘          └───┘ 
src                   └────┘     └────────────────────┘           └───┘
typ                   └────┘    └────────────────────┘          └───┘ 
162    (↑(min a b) : α) = min a b :=
id       └─┘         └─┘  
src      └─┘            └─┘
typ      └─┘         └─┘  
163  by by_cases a ≤ b; simp [min, h]
id                         └─┘  
src     └───────┘    └────┘└─┘└┘ └─
typ     └───────┘  └────┘└─┘└┘└─
doc     └───────┘     └────┘   └┘ └─
txt     └───────┘     └────┘   └┘ └─
par     └───────┘     └────┘   └┘ └─
pid                         └┘ 
st     └──────────────────────────────
164  
src  
typ  
doc  
txt  
par  
pid  
st   
165  end units
166  
167  namespace with_zero
168  open lattice
169  
170  instance [preorder α] : preorder (with_zero α) := with_bot.preorder
id             └──────┘     └──────┘  └───────┘      └───────────────┘
src            └──────┘      └──────┘  └───────┘       └───────────────┘
typ            └──────┘     └──────┘  └───────┘      └───────────────┘
171  instance [partial_order α] : partial_order (with_zero α) := with_bot.partial_order
id             └───────────┘     └───────────┘  └───────┘      └────────────────────┘
src            └───────────┘      └───────────┘  └───────┘       └────────────────────┘
typ            └───────────┘     └───────────┘  └───────┘      └────────────────────┘
172  instance [partial_order α] : order_bot (with_zero α) := with_bot.order_bot
id             └───────────┘     └───────┘  └───────┘      └────────────────┘
src            └───────────┘      └───────┘  └───────┘       └────────────────┘
typ            └───────────┘     └───────┘  └───────┘      └────────────────┘
doc                               └───────┘
173  instance [lattice α] : lattice (with_zero α) := with_bot.lattice
id             └─────┘     └─────┘  └───────┘      └──────────────┘
src            └─────┘      └─────┘  └───────┘       └──────────────┘
typ            └─────┘     └─────┘  └───────┘      └──────────────┘
doc            └─────┘      └─────┘
174  instance [linear_order α] : linear_order (with_zero α) := with_bot.linear_order
id             └──────────┘     └──────────┘  └───────┘      └───────────────────┘
src            └──────────┘      └──────────┘  └───────┘       └───────────────────┘
typ            └──────────┘     └──────────┘  └───────┘      └───────────────────┘
175  instance [decidable_linear_order α] :
id             └────────────────────┘ 
src            └────────────────────┘
typ            └────────────────────┘ 
176   decidable_linear_order (with_zero α) := with_bot.decidable_linear_order
id    └────────────────────┘  └───────┘      └─────────────────────────────┘
src   └────────────────────┘  └───────┘       └─────────────────────────────┘
typ   └────────────────────┘  └───────┘      └─────────────────────────────┘
177  
178  def ordered_comm_monoid [ordered_comm_monoid α]
id                            └─────────────────┘ 
src                           └─────────────────┘
typ                           └─────────────────┘ 
doc                           └─────────────────┘
179    (zero_le : ∀ a : α, 0 ≤ a) : ordered_comm_monoid (with_zero α) :=
id                               └─────────────────┘  └───────┘ 
src                                └─────────────────┘  └───────┘
typ                              └─────────────────┘  └───────┘ 
doc                                 └─────────────────┘
180  begin
st   └─────
181    suffices, refine {
src    └──────┘  └─────┘ 
typ    └──────┘  └─────┘ 
doc    └──────┘  └─────┘ 
txt    └──────┘  └─────┘ 
par    └──────┘  └─────┘ 
pid    └──────┘         
st   ─────────┘└──────────
182      add_le_add_left := this,
id                          └──┘
src  ──────────────────────┘    └─
typ  ──────────────────────┘└──┘└─
doc  ──────────────────────┘    └─
txt  ──────────────────────┘    └─
par  ──────────────────────┘    └─
pid  ──────────────────────┘    └─
st   ─────────────────────────────
183      ..with_zero.partial_order,
id         └─────────────────────┘
src  ─────┘└─────────────────────┘└─
typ  ─────┘└─────────────────────┘└─
doc  ─────┘                       └─
txt  ─────┘                       └─
par  ─────┘                       └─
pid  ─────┘                       └─
st   ───────────────────────────────
184      ..with_zero.add_comm_monoid, .. },
id         └───────────────────────┘
src  ─────┘└───────────────────────┘└────┘
typ  ─────┘└───────────────────────┘└────┘
doc  ─────┘                         └────┘
txt  ─────┘                         └────┘
par  ─────┘                         └────┘
pid  ─────┘                         └────┘
st   ────────────────────────────────────┘└─
185    { intros a b c h,
src      └────────────┘
typ      └────────────┘
doc      └────────────┘
txt      └────────────┘
par      └────────────┘
pid            └──────┘
st   ───┘└────────────┘└─
186      have h' := lt_iff_le_not_le.1 h,
id                  └──────────────┘   
src      └─────────┘└──────────────┘└─┘
typ      └─────────┘└──────────────┘└─┘
doc      └─────────┘                └─┘
txt      └─────────┘                └─┘
par      └─────────┘                └─┘
pid      └─────┘└─┘                └─┘
st   ──────────────────────────────────┘└─
187      rw lt_iff_le_not_le at ⊢,
id          └──────────────┘
src      └─┘└──────────────┘└───┘
typ      └─┘└──────────────┘└───┘
doc      └─┘                └───┘
txt      └─┘                └───┘
par      └─┘                └───┘
pid                        └───┘
st   ───────────────────────────┘└─
188      refine ⟨λ b h₂, _, λ h₂, h'.2 $ this _ _ h₂ _⟩,
id                                └┘     └──┘
src      └─────┘  └────────┘ └───┘  └─┘     └───┘  └─┘
typ      └─────┘  └────────┘ └───┘└┘└─┘ └──┘└───┘  └─┘
doc      └─────┘  └────────┘ └───┘  └─┘     └───┘  └─┘
txt      └─────┘  └────────┘ └───┘  └─┘     └───┘  └─┘
par      └─────┘  └────────┘ └───┘  └─┘     └───┘  └─┘
pid              └────────┘ └───┘  └─┘     └───┘  └─┘
st   ─────────────────────────────────────────────────┘└─
189      cases h₂, cases c with c,
id             └┘        
src      └────┘    └────┘ └─────┘
typ      └────┘└┘  └────┘└─────┘
doc      └────┘    └────┘ └─────┘
txt      └────┘    └────┘ └─────┘
par      └────┘    └────┘ └─────┘
pid                     └─────┘
st   ───────────┘└──────────────┘└─
190      { cases h'.2 (this _ _ bot_le a) },
id               └┘    └──┘     └────┘ 
src        └────┘  └─┘     └───┘└────┘ └┘
typ        └────┘└┘└─┘ └──┘└───┘└────┘└┘
doc        └────┘  └─┘     └───┘       └┘
txt        └────┘  └─┘     └───┘       └┘
par        └────┘  └─┘     └───┘       └┘
pid               └─┘     └───┘       
st   ─────┘└─────────────────────────────┘└┘
191      { refine ⟨_, rfl, _⟩,
id                    └─┘
src        └─────┘ └─┘└─┘└──┘
typ        └─────┘ └─┘└─┘└──┘
doc        └─────┘ └─┘   └──┘
txt        └─────┘ └─┘   └──┘
par        └─────┘ └─┘   └──┘
pid               └─┘   └──┘
st   ───────────────────────┘└─
192        cases a with a,
id               
src        └────┘ └─────┘
typ        └────┘└─────┘
doc        └────┘ └─────┘
txt        └────┘ └─────┘
par        └────┘ └─────┘
pid              └─────┘
st   ───────────────────┘└─
193        { exact with_bot.some_le_some.1 h'.1 },
id                 └───────────────────┘   └┘
src          └────┘└───────────────────┘└─┘  └─┘
typ          └────┘└───────────────────┘└─┘└┘└─┘
doc          └────┘                     └─┘  └─┘
txt          └────┘                     └─┘  └─┘
par          └────┘                     └─┘  └─┘
pid                                    └─┘  └─┘
st   ───────┘└─────────────────────────────────┘└┘
194        { exact le_of_lt (lt_of_add_lt_add_left' $
id                 └──────┘  └────────────────────┘
src          └────┘└──────┘ └────────────────────┘ 
typ          └────┘└──────┘ └────────────────────┘ 
doc          └────┘                                
txt          └────┘                                
par          └────┘                                
pid                                               
st   ─────────────────────────────────────────────────
195            with_bot.some_lt_some.1 h), } } },
id             └───────────────────┘   
src  ─────────┘└───────────────────┘└─┘ 
typ  ─────────┘└───────────────────┘└─┘
doc  ─────────┘                     └─┘ 
txt  ─────────┘                     └─┘ 
par  ─────────┘                     └─┘ 
pid  ─────────┘                     └─┘ 
st   ───────────────────────────────────┘└──────┘
196    { intros a b h c ca h₂,
src      └──────────────────┘
typ      └──────────────────┘
doc      └──────────────────┘
txt      └──────────────────┘
par      └──────────────────┘
pid            └────────────┘
st   ───────────────────────┘└─
197      cases b with b,
id             
src      └────┘ └─────┘
typ      └────┘└─────┘
doc      └────┘ └─────┘
txt      └────┘ └─────┘
par      └────┘ └─────┘
pid            └─────┘
st   ─────────────────┘└─
198      { rw le_antisymm h bot_le at h₂,
id            └─────────┘  └────┘
src        └─┘└─────────┘ └────┘└────┘
typ        └─┘└─────────┘└────┘└────┘
doc        └─┘                  └────┘
txt        └─┘                  └────┘
par        └─┘                  └────┘
pid                            └────┘
st   ─────┘└───────────────────────────┘└─
199        exact ⟨_, h₂, le_refl _⟩ },
id                   └┘  └─────┘
src        └────┘ └─┘  └┘└─────┘└──┘
typ        └────┘ └─┘└┘└┘└─────┘└──┘
doc        └────┘ └─┘  └┘       └──┘
txt        └────┘ └─┘  └┘       └──┘
par        └────┘ └─┘  └┘       └──┘
pid              └─┘  └┘       └─┘
st   ──────────────────────────────┘└┘
200      cases a with a,
id             
src      └────┘ └─────┘
typ      └────┘└─────┘
doc      └────┘ └─────┘
txt      └────┘ └─────┘
par      └────┘ └─────┘
pid            └─────┘
st   ─────────────────┘└─
201      { change c + 0 = some ca at h₂,
id                     └──┘ └┘
src        └─────┘ └─┘└──┘  └────┘
typ        └─────┘└─┘└──┘└┘└────┘
doc        └─────┘  └─┘       └────┘
txt        └─────┘  └─┘       └────┘
par        └─────┘  └─┘       └────┘
pid                └─┘       └───┘
st   ─────┘└──────────────────────────┘└─
202        simp at h₂, simp [h₂],
id                           └┘
src        └────────┘  └────┘  
typ        └────────┘  └────┘└┘
doc        └────────┘  └────┘  
txt        └────────┘  └────┘  
par        └────────┘  └────┘  
pid            └───┘        
st   ───────────────┘└─────────┘└─
203        exact ⟨_, rfl, by simpa using add_le_add_left' (zero_le b)⟩ },
id                   └─┘                 └──────────────┘  └─────┘ 
src        └────┘ └─┘└─┘└┘  └──────────┘└──────────────┘         └┘
typ        └────┘ └─┘└─┘└┘  └──────────┘└──────────────┘ └─────┘└┘
doc        └────┘ └─┘   └┘  └──────────┘                         └┘
txt        └────┘ └─┘   └┘  └──────────┘                         └┘
par        └────┘ └─┘   └┘  └──────────┘                         └┘
pid              └─┘   └┘  └───────────┘                         └┘
st   ──────────────────────┘└───────────────────────────────────────┘└┘└┘
204      { simp at h,
src        └───────┘
typ        └───────┘
doc        └───────┘
txt        └───────┘
par        └───────┘
pid            └──┘
st   ──────────────┘└─
205        cases c with c; change some _ = _ at h₂;
id                               └──┘
src        └────┘ └─────┘  └─────┘└──┘└─┘ └──────┘
typ        └────┘└─────┘  └─────┘└──┘└─┘ └──────┘
doc        └────┘ └─────┘  └─────┘    └─┘ └──────┘
txt        └────┘ └─────┘  └─────┘    └─┘ └──────┘
par        └────┘ └─────┘  └─────┘    └─┘ └──────┘
pid              └─────┘            └─┘ └┘└───┘
st   ───────────────────────────────────────────────
206          simp [-add_comm] at h₂; subst ca; refine ⟨_, rfl, _⟩,
id                                         └┘             └─┘
src          └────────────────────┘  └────┘    └─────┘ └─┘└─┘└──┘
typ          └────────────────────┘  └────┘└┘  └─────┘ └─┘└─┘└──┘
doc          └────────────────────┘  └────┘    └─────┘ └─┘   └──┘
txt          └────────────────────┘  └────┘    └─────┘ └─┘   └──┘
par          └────────────────────┘  └────┘    └─────┘ └─┘   └──┘
pid              └─────────┘└───┘                  └─┘   └──┘
st   ───────────────────────────────────────────────────────────┘└─
207        { exact h },
id                 
src          └────┘ 
typ          └────┘
doc          └────┘ 
txt          └────┘ 
par          └────┘ 
pid                
st   ───────┘└──────┘└┘
208        { exact add_le_add_left' h } } }
id                 └──────────────┘ 
src          └────┘└──────────────┘ 
typ          └────┘└──────────────┘
doc          └────┘                 
txt          └────┘                 
par          └────┘                 
pid                                
st   ────────────────────────────────┘└─────
209  end
st   ──┘
210  
211  end with_zero
212  
213  namespace with_top
214  open lattice
215  
216  instance [add_semigroup α] : add_semigroup (with_top α) :=
id             └───────────┘     └───────────┘  └──────┘ 
src            └───────────┘      └───────────┘  └──────┘
typ            └───────────┘     └───────────┘  └──────┘ 
217  { add := λ o₁ o₂, o₁.bind (λ a, o₂.map (λ b, a + b)),
id              └┘ └┘  └┘└───┘      └┘└──┘        
src                      └───┘         └──┘         
typ             └┘ └┘  └┘└───┘      └┘└──┘        
218    ..@additive.add_semigroup _ $ @with_zero.semigroup (multiplicative α) _ }
id        └────────────────────┘      └─────────────────┘  └────────────┘ 
src       └────────────────────┘      └─────────────────┘  └────────────┘
typ       └────────────────────┘      └─────────────────┘  └────────────┘ 
219  
220  lemma coe_add [add_semigroup α] {a b : α} : ((a + b : α) : with_top α) = a + b := rfl
id                  └───────────┘                         └──────┘          └─┘
src                 └───────────┘                              └──────┘             └─┘
typ                 └───────────┘                         └──────┘          └─┘
221  
222  instance [add_comm_semigroup α] : add_comm_semigroup (with_top α) :=
id             └────────────────┘     └────────────────┘  └──────┘ 
src            └────────────────┘      └────────────────┘  └──────┘
typ            └────────────────┘     └────────────────┘  └──────┘ 
223  { ..@additive.add_comm_semigroup _ $
id        └─────────────────────────┘
src       └─────────────────────────┘
typ       └─────────────────────────┘
224      @with_zero.comm_semigroup (multiplicative α) _ }
id        └──────────────────────┘  └────────────┘ 
src       └──────────────────────┘  └────────────┘
typ       └──────────────────────┘  └────────────┘ 
225  
226  instance [add_monoid α] : add_monoid (with_top α) :=
id             └────────┘     └────────┘  └──────┘ 
src            └────────┘      └────────┘  └──────┘
typ            └────────┘     └────────┘  └──────┘ 
227  { zero := some 0,
id             └──┘
src            └──┘
typ            └──┘
228    add := (+),
id            
src           
typ           
229    ..@additive.add_monoid _ $ @with_zero.monoid (multiplicative α) _ }
id        └─────────────────┘      └──────────────┘  └────────────┘ 
src       └─────────────────┘      └──────────────┘  └────────────┘
typ       └─────────────────┘      └──────────────┘  └────────────┘ 
230  
231  instance [add_comm_monoid α] : add_comm_monoid (with_top α) :=
id             └─────────────┘     └─────────────┘  └──────┘ 
src            └─────────────┘      └─────────────┘  └──────┘
typ            └─────────────┘     └─────────────┘  └──────┘ 
232  { zero := 0,
233    add := (+),
id            
src           
typ           
234    ..@additive.add_comm_monoid _ $
id        └──────────────────────┘
src       └──────────────────────┘
typ       └──────────────────────┘
235      @with_zero.comm_monoid (multiplicative α) _ }
id        └───────────────────┘  └────────────┘ 
src       └───────────────────┘  └────────────┘
typ       └───────────────────┘  └────────────┘ 
236  
237  instance [ordered_comm_monoid α] : ordered_comm_monoid (with_top α) :=
id             └─────────────────┘     └─────────────────┘  └──────┘ 
src            └─────────────────┘      └─────────────────┘  └──────┘
typ            └─────────────────┘     └─────────────────┘  └──────┘ 
doc            └─────────────────┘      └─────────────────┘
238  begin
st   └─────
239    suffices, refine {
src    └──────┘  └─────┘ 
typ    └──────┘  └─────┘ 
doc    └──────┘  └─────┘ 
txt    └──────┘  └─────┘ 
par    └──────┘  └─────┘ 
pid    └──────┘         
st   ─────────┘└──────────
240      add_le_add_left := this,
id                          └──┘
src  ──────────────────────┘    └─
typ  ──────────────────────┘└──┘└─
doc  ──────────────────────┘    └─
txt  ──────────────────────┘    └─
par  ──────────────────────┘    └─
pid  ──────────────────────┘    └─
st   ─────────────────────────────
241      ..with_top.partial_order,
id         └────────────────────┘
src  ─────┘└────────────────────┘└─
typ  ─────┘└────────────────────┘└─
doc  ─────┘                      └─
txt  ─────┘                      └─
par  ─────┘                      └─
pid  ─────┘                      └─
st   ──────────────────────────────
242      ..with_top.add_comm_monoid, ..},
id         └──────────────────────┘
src  ─────┘└──────────────────────┘└───┘
typ  ─────┘└──────────────────────┘└───┘
doc  ─────┘                        └───┘
txt  ─────┘                        └───┘
par  ─────┘                        └───┘
pid  ─────┘                        └───┘
st   ──────────────────────────────────┘└─
243    { intros a b c h,
src      └────────────┘
typ      └────────────┘
doc      └────────────┘
txt      └────────────┘
par      └────────────┘
pid            └──────┘
st   ───┘└────────────┘└─
244      have h' := h,
id                  
src      └─────────┘
typ      └─────────┘
doc      └─────────┘
txt      └─────────┘
par      └─────────┘
pid      └─────┘└─┘
st   ───────────────┘└─
245      rw lt_iff_le_not_le at h' ⊢,
id          └──────────────┘
src      └─┘└──────────────┘└──────┘
typ      └─┘└──────────────┘└──────┘
doc      └─┘                └──────┘
txt      └─┘                └──────┘
par      └─┘                └──────┘
pid                        └──────┘
st   ──────────────────────────────┘└─
246      refine ⟨λ c h₂, _, λ h₂, h'.2 $ this _ _ h₂ _⟩,
id                                └┘     └──┘
src      └─────┘  └────────┘ └───┘  └─┘     └───┘  └─┘
typ      └─────┘  └────────┘ └───┘└┘└─┘ └──┘└───┘  └─┘
doc      └─────┘  └────────┘ └───┘  └─┘     └───┘  └─┘
txt      └─────┘  └────────┘ └───┘  └─┘     └───┘  └─┘
par      └─────┘  └────────┘ └───┘  └─┘     └───┘  └─┘
pid              └────────┘ └───┘  └─┘     └───┘  └─┘
st   ─────────────────────────────────────────────────┘└─
247      cases h₂, cases a with a,
id             └┘        
src      └────┘    └────┘ └─────┘
typ      └────┘└┘  └────┘└─────┘
doc      └────┘    └────┘ └─────┘
txt      └────┘    └────┘ └─────┘
par      └────┘    └────┘ └─────┘
pid                     └─────┘
st   ───────────┘└──────────────┘└─
248      { exact (not_le_of_lt h).elim le_top },
id                └──────────┘        └────┘
src        └────┘ └──────────┘ └─────┘└────┘
typ        └────┘ └──────────┘└─────┘└────┘
doc        └────┘              └─────┘      
txt        └────┘              └─────┘      
par        └────┘              └─────┘      
pid                           └─────┘      
st   ─────┘└─────────────────────────────────┘└┘
249      cases b with b,
id             
src      └────┘ └─────┘
typ      └────┘└─────┘
doc      └────┘ └─────┘
txt      └────┘ └─────┘
par      └────┘ └─────┘
pid            └─────┘
st   ─────────────────┘└─
250      { exact (not_le_of_lt h).elim le_top },
id                └──────────┘        └────┘
src        └────┘ └──────────┘ └─────┘└────┘
typ        └────┘ └──────────┘└─────┘└────┘
doc        └────┘              └─────┘      
txt        └────┘              └─────┘      
par        └────┘              └─────┘      
pid                           └─────┘      
st   ─────┘└─────────────────────────────────┘└┘
251      { exact ⟨_, rfl, le_of_lt (lt_of_add_lt_add_left' $
id                   └─┘  └──────┘  └────────────────────┘
src        └────┘ └─┘└─┘└┘└──────┘ └────────────────────┘ 
typ        └────┘ └─┘└─┘└┘└──────┘ └────────────────────┘ 
doc        └────┘ └─┘   └┘                                
txt        └────┘ └─┘   └┘                                
par        └────┘ └─┘   └┘                                
pid              └─┘   └┘                                
st   ────────────────────────────────────────────────────────
252          with_top.some_lt_some.1 h)⟩ } },
id           └───────────────────┘   
src  ───────┘└───────────────────┘└─┘ └─┘
typ  ───────┘└───────────────────┘└─┘└─┘
doc  ───────┘                     └─┘ └─┘
txt  ───────┘                     └─┘ └─┘
par  ───────┘                     └─┘ └─┘
pid  ───────┘                     └─┘ └┘
st   ───────────────────────────────────┘└──┘
253    { intros a b h c ca h₂,
src      └──────────────────┘
typ      └──────────────────┘
doc      └──────────────────┘
txt      └──────────────────┘
par      └──────────────────┘
pid            └────────────┘
st   ───────────────────────┘└─
254      cases c with c, {cases h₂},
id                             └┘
src      └────┘ └─────┘   └────┘
typ      └────┘└─────┘   └────┘└┘
doc      └────┘ └─────┘   └────┘
txt      └────┘ └─────┘   └────┘
par      └────┘ └─────┘   └────┘
pid            └─────┘        
st   ─────────────────┘└─────────┘└┘
255      cases b with b; cases h₂,
id                            └┘
src      └────┘ └─────┘  └────┘
typ      └────┘└─────┘  └────┘└┘
doc      └────┘ └─────┘  └────┘
txt      └────┘ └─────┘  └────┘
par      └────┘ └─────┘  └────┘
pid            └─────┘       
st   ───────────────────────────┘└─
256      cases a with a, {cases le_antisymm h le_top },
id                             └─────────┘  └────┘
src      └────┘ └─────┘   └────┘└─────────┘ └────┘
typ      └────┘└─────┘   └────┘└─────────┘└────┘
doc      └────┘ └─────┘   └────┘                  
txt      └────┘ └─────┘   └────┘                  
par      └────┘ └─────┘   └────┘                  
pid            └─────┘                          
st   ─────────────────┘└────────────────────────────┘└┘
257      simp at h,
src      └───────┘
typ      └───────┘
doc      └───────┘
txt      └───────┘
par      └───────┘
pid          └──┘
st   ────────────┘└─
258      exact ⟨_, rfl, add_le_add_left' h⟩, }
id                 └─┘  └──────────────┘ 
src      └────┘ └─┘└─┘└┘└──────────────┘ 
typ      └────┘ └─┘└─┘└┘└──────────────┘
doc      └────┘ └─┘   └┘                 
txt      └────┘ └─┘   └┘                 
par      └────┘ └─┘   └┘                 
pid            └─┘   └┘                 
st   ─────────────────────────────────────┘└───
259  end
st   ──┘
260  
261  @[simp] lemma zero_lt_top [ordered_comm_monoid α] : (0 : with_top α) < ⊤ :=
id                              └─────────────────┘          └──────┘    
src                             └─────────────────┘           └──────┘     
typ                             └─────────────────┘          └──────┘    
doc    └──┘                     └─────────────────┘
262  coe_lt_top 0
id   └────────┘
src  └────────┘
typ  └────────┘
263  
264  @[simp] lemma zero_lt_coe [ordered_comm_monoid α] (a : α) : (0 : with_top α) < a ↔ 0 < a :=
id                              └─────────────────┘                 └──────┘         
src                             └─────────────────┘                   └──────┘          
typ                             └─────────────────┘                 └──────┘         
doc    └──┘                     └─────────────────┘
265  coe_lt_coe
id   └────────┘
src  └────────┘
typ  └────────┘
266  
267  @[simp] lemma add_top [ordered_comm_monoid α] : ∀{a : with_top α}, a + ⊤ = ⊤
id                          └─────────────────┘          └──────┘        
src                         └─────────────────┘            └──────┘          
typ                         └─────────────────┘          └──────┘        
doc    └──┘                 └─────────────────┘
268  | none := rfl
id     └──┘    └─┘
src    └──┘    └─┘
typ    └──┘    └─┘
269  | (some a) := rfl
id      └──┘       └─┘
src     └──┘       └─┘
typ     └──┘       └─┘
270  
271  @[simp] lemma top_add [ordered_comm_monoid α] {a : with_top α} : ⊤ + a = ⊤ := rfl
id                          └─────────────────┘        └──────┘             └─┘
src                         └─────────────────┘         └──────┘               └─┘
typ                         └─────────────────┘        └──────┘             └─┘
doc    └──┘                 └─────────────────┘
272  
273  lemma add_eq_top [ordered_comm_monoid α] (a b : with_top α) : a + b = ⊤ ↔ a = ⊤ ∨ b = ⊤ :=
id                     └─────────────────┘          └──────┘                 
src                    └─────────────────┘           └──────┘                      
typ                    └─────────────────┘          └──────┘                 
doc                    └─────────────────┘
274  by cases a; cases b; simp [none_eq_top, some_eq_coe, coe_add.symm]
id                            └─────────┘  └─────────┘
src     └────┘   └────┘   └────┘└─────────┘└┘└─────────┘└┘            └─
typ     └────┘  └────┘  └────┘└─────────┘└┘└─────────┘└┘└──────────┘└─
doc     └────┘   └────┘   └────┘           └┘           └┘            └─
txt     └────┘   └────┘   └────┘           └┘           └┘            └─
par     └────┘   └────┘   └────┘           └┘           └┘            └─
pid                                    └┘           └┘            
st     └────────────────────────────────────────────────────────────────
275  
src  
typ  
doc  
txt  
par  
pid  
st   
276  lemma add_lt_top [ordered_comm_monoid α] (a b : with_top α) : a + b < ⊤ ↔ a < ⊤ ∧ b < ⊤ :=
id                     └─────────────────┘          └──────┘                 
src                    └─────────────────┘           └──────┘                      
typ                    └─────────────────┘          └──────┘                 
doc                    └─────────────────┘
277  begin
st   └─────
278    apply not_iff_not.1,
id           └─────────┘
src    └────┘└─────────┘└┘
typ    └────┘└─────────┘└┘
doc    └────┘           └┘
txt    └────┘           └┘
par    └────┘           └┘
pid                    └┘
st   ────────────────────┘└─
279    simp [lt_top_iff_ne_top, add_eq_top],
id           └───────────────┘  └────────┘
src    └────┘└───────────────┘└┘└────────┘
typ    └────┘└───────────────┘└┘└────────┘
doc    └────┘                 └┘          
txt    └────┘                 └┘          
par    └────┘                 └┘          
pid                         └┘          
st   ─────────────────────────────────────┘└─
280    finish,
src    └────┘
typ    └────┘
doc    └────┘
txt    └────┘
par    └────┘
st   ───────┘└─
281    apply classical.dec _,
id           └───────────┘
src    └────┘└───────────┘└┘
typ    └────┘└───────────┘└┘
doc    └────┘             └┘
txt    └────┘             └┘
par    └────┘             └┘
pid                      └┘
st   ──────────────────────┘└─
282    apply classical.dec _,
id           └───────────┘
src    └────┘└───────────┘└┘
typ    └────┘└───────────┘└┘
doc    └────┘             └┘
txt    └────┘             └┘
par    └────┘             └┘
pid                      └┘
st   ──────────────────────┘└─
283  end
st   ──┘
284  
285  instance [canonically_ordered_monoid α] : canonically_ordered_monoid (with_top α) :=
id             └────────────────────────┘     └────────────────────────┘  └──────┘ 
src            └────────────────────────┘      └────────────────────────┘  └──────┘
typ            └────────────────────────┘     └────────────────────────┘  └──────┘ 
doc            └────────────────────────┘      └────────────────────────┘
286  { le_iff_exists_add := assume a b,
id                                  
typ                                 
287    match a, b with
id             
typ            
288    | a, none     := show a ≤ ⊤ ↔ ∃c, ⊤ = a + c, by simp; refine ⟨⊤, _⟩; cases a; refl
id         └──┘                                                       
src         └──┘                               └──┘  └─────┘ └──┘  └────┘   └────
typ        └──┘                             └──┘  └─────┘ └──┘  └────┘  └────
doc                                                    └──┘  └─────┘  └──┘  └────┘   └────
txt                                                    └──┘  └─────┘  └──┘  └────┘   └────
par                                                    └──┘  └─────┘  └──┘  └────┘   └────
pid                                                                  └──┘              
st                                                    └───────────────────────────────────
289    | (some a), (some b) := show (a:with_top α) ≤ ↑b ↔ ∃c:with_top α, ↑b = ↑a + c,
id                 └──┘              └──────┘         └──────┘        
src  ─┘             └──┘               └──────┘          └──────┘        
typ  ─┘            └──┘              └──────┘         └──────┘        
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
290      begin
st       └─────
291        simp [canonically_ordered_monoid.le_iff_exists_add, -add_comm],
id               └──────────────────────────────────────────┘
src        └────┘└──────────────────────────────────────────┘└──────────┘
typ        └────┘└──────────────────────────────────────────┘└──────────┘
doc        └────┘                                            └──────────┘
txt        └────┘                                            └──────────┘
par        └────┘                                            └──────────┘
pid                                                        └──────────┘
st   ───────────────────────────────────────────────────────────────────┘└─
292        split,
src        └───┘
typ        └───┘
doc        └───┘
txt        └───┘
par        └───┘
st   ──────────┘└─
293        { rintro ⟨c, rfl⟩, refine ⟨c, _⟩, simp [coe_add] },
id                                                └─────┘
src          └─────────────┘  └─────┘  └──┘  └────┘└─────┘└┘
typ          └─────────────┘  └─────┘ └──┘  └────┘└─────┘└┘
doc          └─────────────┘  └─────┘  └──┘  └────┘       └┘
txt          └─────────────┘  └─────┘  └──┘  └────┘       └┘
par          └─────────────┘  └─────┘  └──┘  └────┘       └┘
pid                └───────┘          └──┘             
st   ───────┘└─────────────┘└─────────────┘└───────────────┘└┘
294        { exact assume h, match b, h with _, ⟨some c, rfl⟩ := ⟨_, rfl⟩ end }
id                                              └──┘                └─┘
src          └────┘      └──┘      └┘ └───────┘ └──┘ └┘   └───┘ └─┘└─┘└────┘
typ          └────┘      └──┘     └┘ └───────┘ └──┘ └┘   └───┘ └─┘└─┘└────┘
doc          └────┘      └──┘      └┘ └───────┘      └┘   └───┘ └─┘   └────┘
txt          └────┘      └──┘      └┘ └───────┘      └┘   └───┘ └─┘   └────┘
par          └────┘      └──┘      └┘ └───────┘      └┘   └───┘ └─┘   └────┘
pid                     └──┘      └┘ └───────┘      └┘   └───┘ └─┘   └───┘
st   ────────────────────────────────────────────────────────────────────────┘└─
295      end
st   ──────┘
296    | none, some b := show (⊤ : with_top α) ≤ b ↔ ∃c:with_top α, ↑b = ⊤ + c, by simp
id       └──┘  └──┘              └──────┘         └──────┘       
src      └──┘  └──┘               └──────┘          └──────┘              └────
typ      └──┘  └──┘              └──────┘         └──────┘            └────
doc                                                                                └────
txt                                                                                └────
par                                                                                └────
pid                                                                                    
st                                                                                └─────
297    end,
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
298    .. with_top.order_bot,
id        └────────────────┘
src       └────────────────┘
typ       └────────────────┘
299    .. with_top.ordered_comm_monoid }
id        └──────────────────────────┘
src       └──────────────────────────┘
typ       └──────────────────────────┘
300  
301  end with_top
302  
303  namespace with_bot
304  open lattice
305  
306  instance [add_semigroup α] : add_semigroup (with_bot α) := with_top.add_semigroup
id             └───────────┘     └───────────┘  └──────┘      └────────────────────┘
src            └───────────┘      └───────────┘  └──────┘       └────────────────────┘
typ            └───────────┘     └───────────┘  └──────┘      └────────────────────┘
307  instance [add_comm_semigroup α] : add_comm_semigroup (with_bot α) := with_top.add_comm_semigroup
id             └────────────────┘     └────────────────┘  └──────┘      └─────────────────────────┘
src            └────────────────┘      └────────────────┘  └──────┘       └─────────────────────────┘
typ            └────────────────┘     └────────────────┘  └──────┘      └─────────────────────────┘
308  instance [add_monoid α] : add_monoid (with_bot α) := with_top.add_monoid
id             └────────┘     └────────┘  └──────┘      └─────────────────┘
src            └────────┘      └────────┘  └──────┘       └─────────────────┘
typ            └────────┘     └────────┘  └──────┘      └─────────────────┘
309  instance [add_comm_monoid α] : add_comm_monoid (with_bot α) :=  with_top.add_comm_monoid
id             └─────────────┘     └─────────────┘  └──────┘       └──────────────────────┘
src            └─────────────┘      └─────────────┘  └──────┘        └──────────────────────┘
typ            └─────────────┘     └─────────────┘  └──────┘       └──────────────────────┘
310  
311  instance [ordered_comm_monoid α] : ordered_comm_monoid (with_bot α) :=
id             └─────────────────┘     └─────────────────┘  └──────┘ 
src            └─────────────────┘      └─────────────────┘  └──────┘
typ            └─────────────────┘     └─────────────────┘  └──────┘ 
doc            └─────────────────┘      └─────────────────┘
312  begin
st   └─────
313    suffices, refine {
src    └──────┘  └─────┘ 
typ    └──────┘  └─────┘ 
doc    └──────┘  └─────┘ 
txt    └──────┘  └─────┘ 
par    └──────┘  └─────┘ 
pid    └──────┘         
st   ─────────┘└──────────
314      add_le_add_left := this,
id                          └──┘
src  ──────────────────────┘    └─
typ  ──────────────────────┘└──┘└─
doc  ──────────────────────┘    └─
txt  ──────────────────────┘    └─
par  ──────────────────────┘    └─
pid  ──────────────────────┘    └─
st   ─────────────────────────────
315      ..with_bot.partial_order,
id         └────────────────────┘
src  ─────┘└────────────────────┘└─
typ  ─────┘└────────────────────┘└─
doc  ─────┘                      └─
txt  ─────┘                      └─
par  ─────┘                      └─
pid  ─────┘                      └─
st   ──────────────────────────────
316      ..with_bot.add_comm_monoid, ..},
id         └──────────────────────┘
src  ─────┘└──────────────────────┘└───┘
typ  ─────┘└──────────────────────┘└───┘
doc  ─────┘                        └───┘
txt  ─────┘                        └───┘
par  ─────┘                        └───┘
pid  ─────┘                        └───┘
st   ──────────────────────────────────┘└─
317    { intros a b c h,
src      └────────────┘
typ      └────────────┘
doc      └────────────┘
txt      └────────────┘
par      └────────────┘
pid            └──────┘
st   ───┘└────────────┘└─
318      have h' := h,
id                  
src      └─────────┘
typ      └─────────┘
doc      └─────────┘
txt      └─────────┘
par      └─────────┘
pid      └─────┘└─┘
st   ───────────────┘└─
319      rw lt_iff_le_not_le at h' ⊢,
id          └──────────────┘
src      └─┘└──────────────┘└──────┘
typ      └─┘└──────────────┘└──────┘
doc      └─┘                └──────┘
txt      └─┘                └──────┘
par      └─┘                └──────┘
pid                        └──────┘
st   ──────────────────────────────┘└─
320      refine ⟨λ b h₂, _, λ h₂, h'.2 $ this _ _ h₂ _⟩,
id                                └┘     └──┘
src      └─────┘  └────────┘ └───┘  └─┘     └───┘  └─┘
typ      └─────┘  └────────┘ └───┘└┘└─┘ └──┘└───┘  └─┘
doc      └─────┘  └────────┘ └───┘  └─┘     └───┘  └─┘
txt      └─────┘  └────────┘ └───┘  └─┘     └───┘  └─┘
par      └─────┘  └────────┘ └───┘  └─┘     └───┘  └─┘
pid              └────────┘ └───┘  └─┘     └───┘  └─┘
st   ─────────────────────────────────────────────────┘└─
321      cases h₂, cases a with a,
id             └┘        
src      └────┘    └────┘ └─────┘
typ      └────┘└┘  └────┘└─────┘
doc      └────┘    └────┘ └─────┘
txt      └────┘    └────┘ └─────┘
par      └────┘    └────┘ └─────┘
pid                     └─────┘
st   ───────────┘└──────────────┘└─
322      { exact (not_le_of_lt h).elim bot_le },
id                └──────────┘        └────┘
src        └────┘ └──────────┘ └─────┘└────┘
typ        └────┘ └──────────┘└─────┘└────┘
doc        └────┘              └─────┘      
txt        └────┘              └─────┘      
par        └────┘              └─────┘      
pid                           └─────┘      
st   ─────┘└─────────────────────────────────┘└┘
323      cases c with c,
id             
src      └────┘ └─────┘
typ      └────┘└─────┘
doc      └────┘ └─────┘
txt      └────┘ └─────┘
par      └────┘ └─────┘
pid            └─────┘
st   ─────────────────┘└─
324      { exact (not_le_of_lt h).elim bot_le },
id                └──────────┘        └────┘
src        └────┘ └──────────┘ └─────┘└────┘
typ        └────┘ └──────────┘└─────┘└────┘
doc        └────┘              └─────┘      
txt        └────┘              └─────┘      
par        └────┘              └─────┘      
pid                           └─────┘      
st   ─────┘└─────────────────────────────────┘└┘
325      { exact ⟨_, rfl, le_of_lt (lt_of_add_lt_add_left' $
id                   └─┘  └──────┘  └────────────────────┘
src        └────┘ └─┘└─┘└┘└──────┘ └────────────────────┘ 
typ        └────┘ └─┘└─┘└┘└──────┘ └────────────────────┘ 
doc        └────┘ └─┘   └┘                                
txt        └────┘ └─┘   └┘                                
par        └────┘ └─┘   └┘                                
pid              └─┘   └┘                                
st   ────────────────────────────────────────────────────────
326          with_bot.some_lt_some.1 h)⟩ } },
id           └───────────────────┘   
src  ───────┘└───────────────────┘└─┘ └─┘
typ  ───────┘└───────────────────┘└─┘└─┘
doc  ───────┘                     └─┘ └─┘
txt  ───────┘                     └─┘ └─┘
par  ───────┘                     └─┘ └─┘
pid  ───────┘                     └─┘ └┘
st   ───────────────────────────────────┘└──┘
327    { intros a b h c ca h₂,
src      └──────────────────┘
typ      └──────────────────┘
doc      └──────────────────┘
txt      └──────────────────┘
par      └──────────────────┘
pid            └────────────┘
st   ───────────────────────┘└─
328      cases c with c, {cases h₂},
id                             └┘
src      └────┘ └─────┘   └────┘
typ      └────┘└─────┘   └────┘└┘
doc      └────┘ └─────┘   └────┘
txt      └────┘ └─────┘   └────┘
par      └────┘ └─────┘   └────┘
pid            └─────┘        
st   ─────────────────┘└─────────┘└┘
329      cases a with a; cases h₂,
id                            └┘
src      └────┘ └─────┘  └────┘
typ      └────┘└─────┘  └────┘└┘
doc      └────┘ └─────┘  └────┘
txt      └────┘ └─────┘  └────┘
par      └────┘ └─────┘  └────┘
pid            └─────┘       
st   ───────────────────────────┘└─
330      cases b with b, {cases le_antisymm h bot_le},
id                             └─────────┘  └────┘
src      └────┘ └─────┘   └────┘└─────────┘ └────┘
typ      └────┘└─────┘   └────┘└─────────┘└────┘
doc      └────┘ └─────┘   └────┘            
txt      └────┘ └─────┘   └────┘            
par      └────┘ └─────┘   └────┘            
pid            └─────┘                    
st   ─────────────────┘└───────────────────────────┘└┘
331      simp at h,
src      └───────┘
typ      └───────┘
doc      └───────┘
txt      └───────┘
par      └───────┘
pid          └──┘
st   ────────────┘└─
332      exact ⟨_, rfl, add_le_add_left' h⟩, }
id                 └─┘  └──────────────┘ 
src      └────┘ └─┘└─┘└┘└──────────────┘ 
typ      └────┘ └─┘└─┘└┘└──────────────┘
doc      └────┘ └─┘   └┘                 
txt      └────┘ └─┘   └┘                 
par      └────┘ └─┘   └┘                 
pid            └─┘   └┘                 
st   ─────────────────────────────────────┘└───
333  end
st   ──┘
334  
335  @[simp] lemma coe_zero [add_monoid α] : ((0 : α) : with_bot α) = 0 := rfl
id                           └────────┘               └──────┘         └─┘
src                          └────────┘                 └──────┘          └─┘
typ                          └────────┘               └──────┘         └─┘
doc    └──┘
336  
337  @[simp] lemma coe_add [add_semigroup α] (a b : α) : ((a + b : α) : with_bot α) = a + b := rfl
id                          └───────────┘                         └──────┘          └─┘
src                         └───────────┘                              └──────┘             └─┘
typ                         └───────────┘                         └──────┘          └─┘
doc    └──┘
338  
339  @[simp] lemma bot_add [ordered_comm_monoid α] (a : with_bot α) : ⊥ + a = ⊥ := rfl
id                          └─────────────────┘        └──────┘             └─┘
src                         └─────────────────┘         └──────┘               └─┘
typ                         └─────────────────┘        └──────┘             └─┘
doc    └──┘                 └─────────────────┘
340  
341  @[simp] lemma add_bot [ordered_comm_monoid α] (a : with_bot α) : a + ⊥ = ⊥ := by cases a; refl
id                          └─────────────────┘        └──────┘                      
src                         └─────────────────┘         └──────┘                  └────┘   └────
typ                         └─────────────────┘        └──────┘                └────┘  └────
doc    └──┘                 └─────────────────┘                                       └────┘   └────
txt                                                                                   └────┘   └────
par                                                                                   └────┘   └────
pid                                                                                               
st                                                                                   └──────────────
342  
src  
typ  
doc  
txt  
par  
pid  
st   
343  instance has_one [has_one α] : has_one (with_bot α) := ⟨(1 : α)⟩
id                     └─────┘     └─────┘  └──────┘            
src                    └─────┘      └─────┘  └──────┘
typ                    └─────┘     └─────┘  └──────┘            
344  
345  @[simp] lemma coe_one [has_one α] : ((1 : α) : with_bot α) = 1 := rfl
id                          └─────┘               └──────┘         └─┘
src                         └─────┘                 └──────┘          └─┘
typ                         └─────┘               └──────┘         └─┘
doc    └──┘
346  
347  end with_bot
348  
349  section canonically_ordered_monoid
350  variables [canonically_ordered_monoid α] {a b c d : α}
id              └────────────────────────┘
src             └────────────────────────┘
typ             └────────────────────────┘
doc             └────────────────────────┘
351  
352  lemma le_iff_exists_add : a ≤ b ↔ ∃c, b = a + c :=
id                                      
src                                         
typ                                     
353  canonically_ordered_monoid.le_iff_exists_add a b
id   └──────────────────────────────────────────┘  
src  └──────────────────────────────────────────┘
typ  └──────────────────────────────────────────┘  
354  
355  @[simp] lemma zero_le (a : α) : 0 ≤ a := le_iff_exists_add.mpr ⟨a, by simp⟩
id                                         └───────────────┘└──┘  
src                                          └───────────────┘└──┘        └──┘
typ                                        └───────────────┘└──┘       └──┘
doc    └──┘                                                                └──┘
txt                                                                        └──┘
par                                                                        └──┘
st                                                                        └───┘
356  
357  lemma bot_eq_zero : (⊥ : α) = 0 :=
id                             
src                             
typ                            
358  le_antisymm lattice.bot_le (zero_le ⊥)
id   └─────────┘ └────────────┘  └─────┘ 
src  └─────────┘ └────────────┘  └─────┘ 
typ  └─────────┘ └────────────┘  └─────┘ 
359  
360  @[simp] lemma add_eq_zero_iff : a + b = 0 ↔ a = 0 ∧ b = 0 :=
id                                                
src                                                   
typ                                               
doc    └──┘
361  add_eq_zero_iff' (zero_le _) (zero_le _)
id   └──────────────┘  └─────┘     └─────┘
src  └──────────────┘  └─────┘     └─────┘
typ  └──────────────┘  └─────┘     └─────┘
362  
363  @[simp] lemma le_zero_iff_eq : a ≤ 0 ↔ a = 0 :=
id                                        
src                                         
typ                                       
doc    └──┘
364  iff.intro
id   └───────┘
src  └───────┘
typ  └───────┘
365    (assume h, le_antisymm h (zero_le a))
id               └─────────┘   └─────┘ 
src               └─────────┘    └─────┘
typ              └─────────┘   └─────┘ 
366    (assume h, h ▸ le_refl a)
id                 └─────┘ 
src                  └─────┘
typ                └─────┘ 
367  
368  protected lemma zero_lt_iff_ne_zero : 0 < a ↔ a ≠ 0 :=
id                                               
src                                                
typ                                              
369  iff.intro ne_of_gt $ assume hne, lt_of_le_of_ne (zero_le _) hne.symm
id   └───────┘ └──────┘          └─┘  └────────────┘  └─────┘    └─┘└───┘
src  └───────┘ └──────┘               └────────────┘  └─────┘       └───┘
typ  └───────┘ └──────┘          └─┘  └────────────┘  └─────┘    └─┘└───┘
370  
371  lemma le_add_left (h : a ≤ c) : a ≤ b + c :=
id                                    
src                                      
typ                                   
372  calc a = 0 + a : by simp
id              
src                     └────
typ                   └────
doc                      └────
txt                      └────
par                      └────
pid                          
st                      └─────
373    ... ≤ b + c : add_le_add' (zero_le _) h
id                └─────────┘  └─────┘    
src  ─┘             └─────────┘  └─────┘
typ  ─┘           └─────────┘  └─────┘    
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
374  
375  lemma le_add_right (h : a ≤ b) : a ≤ b + c :=
id                                     
src                                       
typ                                    
376  calc a = a + 0 : by simp
id            
src                     └────
typ                   └────
doc                      └────
txt                      └────
par                      └────
pid                          
st                      └─────
377    ... ≤ b + c : add_le_add' h (zero_le _)
id                └─────────┘   └─────┘
src  ─┘             └─────────┘    └─────┘
typ  ─┘           └─────────┘   └─────┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
378  
379  instance with_zero.canonically_ordered_monoid :
380    canonically_ordered_monoid (with_zero α) :=
id     └────────────────────────┘  └───────┘ 
src    └────────────────────────┘  └───────┘
typ    └────────────────────────┘  └───────┘ 
doc    └────────────────────────┘
381  { le_iff_exists_add := λ a b, begin
id                             
typ                            
st                                 └─────
382      cases a with a,
id             
src      └────┘ └─────┘
typ      └────┘└─────┘
doc      └────┘ └─────┘
txt      └────┘ └─────┘
par      └────┘ └─────┘
pid            └─────┘
st   ─────────────────┘└─
383      { exact iff_of_true lattice.bot_le ⟨b, (zero_add b).symm⟩ },
id               └─────────┘ └────────────┘      └──────┘ 
src        └────┘└─────────┘└────────────┘  └┘ └──────┘ └──────┘
typ        └────┘└─────────┘└────────────┘  └┘ └──────┘└──────┘
doc        └────┘                           └┘          └──────┘
txt        └────┘                           └┘          └──────┘
par        └────┘                           └┘          └──────┘
pid                                        └┘          └─────┘
st   ─────┘└──────────────────────────────────────────────────────┘└┘
384      cases b with b,
id             
src      └────┘ └─────┘
typ      └────┘└─────┘
doc      └────┘ └─────┘
txt      └────┘ └─────┘
par      └────┘ └─────┘
pid            └─────┘
st   ─────────────────┘└─
385      { exact iff_of_false
id               └──────────┘
src        └────┘└──────────┘
typ        └────┘└──────────┘
doc        └────┘            
txt        └────┘            
par        └────┘            
pid                         
st   ─────┘└──────────────────
386          (mt (le_antisymm lattice.bot_le) (by simp))
id            └┘  └─────────┘ └────────────┘
src  ───────┘ └┘ └─────────┘└────────────┘└┘   └──┘└──
typ  ───────┘ └┘ └─────────┘└────────────┘└┘   └──┘└──
doc  ───────┘                             └┘   └──┘└──
txt  ───────┘                             └┘   └──┘└──
par  ───────┘                             └┘   └──┘└──
pid  ───────┘                             └┘   └───────
st   ───────────────────────────────────────────┘└───┘└──
387          (λ ⟨c, h⟩, by cases c; cases h) },
id                                       
src  ───────┘  └┘ └┘ └─┘  └────┘ └┘└────┘ └┘
typ  ───────┘  └┘ └┘ └─┘  └────┘└┘└────┘└┘
doc  ───────┘  └┘ └┘ └─┘  └────┘ └┘└────┘ └┘
txt  ───────┘  └┘ └┘ └─┘  └────┘ └┘└────┘ └┘
par  ───────┘  └┘ └┘ └─┘  └────┘ └┘└────┘ └┘
pid  ───────┘  └┘ └┘ └─┘  └─────┘ └──────┘ 
st   ────────────────────┘└───────────────┘└┘└┘
388      { simp [le_iff_exists_add, -add_comm],
id               └───────────────┘
src        └────┘└───────────────┘└──────────┘
typ        └────┘└───────────────┘└──────────┘
doc        └────┘                 └──────────┘
txt        └────┘                 └──────────┘
par        └────┘                 └──────────┘
pid                             └──────────┘
st   ────────────────────────────────────────┘└─
389        split; intro h; rcases h with ⟨c, h⟩,
id                                
src        └───┘  └─────┘  └─────┘ └──────────┘
typ        └───┘  └─────┘  └─────┘└──────────┘
doc        └───┘  └─────┘  └─────┘ └──────────┘
txt        └───┘  └─────┘  └─────┘ └──────────┘
par        └───┘  └─────┘  └─────┘ └──────────┘
pid                    └┘         └──────────┘
st   ─────────────────────────────────────────┘└─
390        { exact ⟨some c, congr_arg some h⟩ },
id                         └───────┘ └──┘ 
src          └────┘      └┘└───────┘└──┘ └┘
typ          └────┘     └┘└───────┘└──┘└┘
doc          └────┘      └┘              └┘
txt          └────┘      └┘              └┘
par          └────┘      └┘              └┘
pid                     └┘              
st   ───────┘└───────────────────────────────┘└┘
391        { cases c; cases h,
id                         
src          └────┘   └────┘
typ          └────┘  └────┘
doc          └────┘   └────┘
txt          └────┘   └────┘
par          └────┘   └────┘
pid                       
st   ───────────────────────┘└─
392          { exact ⟨_, (add_zero _).symm⟩ },
id                        └──────┘
src            └────┘ └─┘ └──────┘└────────┘
typ            └────┘ └─┘ └──────┘└────────┘
doc            └────┘ └─┘         └────────┘
txt            └────┘ └─┘         └────────┘
par            └────┘ └─┘         └────────┘
pid                  └─┘         └───────┘
st   ─────────┘└───────────────────────────┘└┘
393          { exact ⟨_, rfl⟩ } } }
id                       └─┘
src            └────┘ └─┘└─┘└┘
typ            └────┘ └─┘└─┘└┘
doc            └────┘ └─┘   └┘
txt            └────┘ └─┘   └┘
par            └────┘ └─┘   └┘
pid                  └─┘   
st   ────────────────────────┘└─────
394    end,
st   ────┘
395    bot    := 0,
396    bot_le := assume a a' h, option.no_confusion h,
id                       └┘   └─────────────────┘ 
src                             └─────────────────┘
typ                      └┘   └─────────────────┘ 
397    .. with_zero.ordered_comm_monoid zero_le }
id        └───────────────────────────┘ └─────┘
src       └───────────────────────────┘ └─────┘
typ       └───────────────────────────┘ └─────┘
398  
399  end canonically_ordered_monoid
400  
401  @[priority 100] -- see Note [lower instance priority]
402  instance ordered_cancel_comm_monoid.to_ordered_comm_monoid
403    [H : ordered_cancel_comm_monoid α] : ordered_comm_monoid α :=
id          └────────────────────────┘     └─────────────────┘ 
src         └────────────────────────┘      └─────────────────┘
typ         └────────────────────────┘     └─────────────────┘ 
doc                                         └─────────────────┘
404  { lt_of_add_lt_add_left := @lt_of_add_lt_add_left _ _, ..H }
id                               └───────────────────┘        
src                              └───────────────────┘
typ                              └───────────────────┘        
405  
406  section ordered_cancel_comm_monoid
407  variables [ordered_cancel_comm_monoid α] {a b c x y : α}
id              └────────────────────────┘
src             └────────────────────────┘
typ             └────────────────────────┘
408  
409  @[simp] lemma add_le_add_iff_left (a : α) {b c : α} : a + b ≤ a + c ↔ b ≤ c :=
id                                                                 
src                                                                      
typ                                                                
doc    └──┘
410  ⟨le_of_add_le_add_left, λ h, add_le_add_left h _⟩
id    └───────────────────┘      └─────────────┘ 
src   └───────────────────┘       └─────────────┘
typ   └───────────────────┘      └─────────────┘ 
411  
412  @[simp] lemma add_le_add_iff_right (c : α) : a + c ≤ b + c ↔ a ≤ b :=
id                                                         
src                                                             
typ                                                        
doc    └──┘
413  add_comm c a ▸ add_comm c b ▸ add_le_add_iff_left c
id   └──────┘    └──────┘    └─────────────────┘ 
src  └──────┘      └──────┘      └─────────────────┘
typ  └──────┘    └──────┘    └─────────────────┘ 
414  
415  @[simp] lemma add_lt_add_iff_left (a : α) {b c : α} : a + b < a + c ↔ b < c :=
id                                                                 
src                                                                      
typ                                                                
doc    └──┘
416  ⟨lt_of_add_lt_add_left, λ h, add_lt_add_left h _⟩
id    └───────────────────┘      └─────────────┘ 
src   └───────────────────┘       └─────────────┘
typ   └───────────────────┘      └─────────────┘ 
417  
418  @[simp] lemma add_lt_add_iff_right (c : α) : a + c < b + c ↔ a < b :=
id                                                         
src                                                             
typ                                                        
doc    └──┘
419  add_comm c a ▸ add_comm c b ▸ add_lt_add_iff_left c
id   └──────┘    └──────┘    └─────────────────┘ 
src  └──────┘      └──────┘      └─────────────────┘
typ  └──────┘    └──────┘    └─────────────────┘ 
420  
421  @[simp] lemma le_add_iff_nonneg_right (a : α) {b : α} : a ≤ a + b ↔ 0 ≤ b :=
id                                                                  
src                                                                     
typ                                                                 
doc    └──┘
422  have a + 0 ≤ a + b ↔ 0 ≤ b, from add_le_add_iff_left a,
id                           └─────────────────┘ 
src                              └─────────────────┘
typ                          └─────────────────┘ 
423  by rwa add_zero at this
id          └──────┘
src     └──┘└──────┘└────────
typ     └──┘└──────┘└────────
doc     └──┘        └────────
txt     └──┘        └────────
par     └──┘        └────────
pid                └──────┘
st     └─────────────────────
424  
src  
typ  
doc  
txt  
par  
pid  
st   
425  @[simp] lemma le_add_iff_nonneg_left (a : α) {b : α} : a ≤ b + a ↔ 0 ≤ b :=
id                                                                 
src                                                                    
typ                                                                
doc    └──┘
426  by rw [add_comm, le_add_iff_nonneg_right]
id          └──────┘  └─────────────────────┘
src     └──┘└──────┘└┘└─────────────────────┘└─
typ     └──┘└──────┘└┘└─────────────────────┘└─
doc     └──┘        └┘                       └─
txt     └──┘        └┘                       └─
par     └──┘        └┘                       └─
pid       └┘        └┘                       
st     └───────────┘└───────────────────────┘
427  
src  
typ  
doc  
txt  
par  
pid  
st   
428  @[simp] lemma lt_add_iff_pos_right (a : α) {b : α} : a < a + b ↔ 0 < b :=
id                                                               
src                                                                  
typ                                                              
doc    └──┘
429  have a + 0 < a + b ↔ 0 < b, from add_lt_add_iff_left a,
id                           └─────────────────┘ 
src                              └─────────────────┘
typ                          └─────────────────┘ 
430  by rwa add_zero at this
id          └──────┘
src     └──┘└──────┘└────────
typ     └──┘└──────┘└────────
doc     └──┘        └────────
txt     └──┘        └────────
par     └──┘        └────────
pid                └──────┘
st     └─────────────────────
431  
src  
typ  
doc  
txt  
par  
pid  
st   
432  @[simp] lemma lt_add_iff_pos_left (a : α) {b : α} : a < b + a ↔ 0 < b :=
id                                                              
src                                                                 
typ                                                             
doc    └──┘
433  by rw [add_comm, lt_add_iff_pos_right]
id          └──────┘  └──────────────────┘
src     └──┘└──────┘└┘└──────────────────┘└─
typ     └──┘└──────┘└┘└──────────────────┘└─
doc     └──┘        └┘                    └─
txt     └──┘        └┘                    └─
par     └──┘        └┘                    └─
pid       └┘        └┘                    
st     └───────────┘└────────────────────┘
434  
src  
typ  
doc  
txt  
par  
pid  
st   
435  @[simp] lemma add_le_iff_nonpos_left : x + y ≤ y ↔ x ≤ 0 :=
id                                                 
src                                                    
typ                                                
doc    └──┘
436  by { convert add_le_add_iff_right y, rw [zero_add] }
id                └──────────────────┘       └──────┘
src       └──────┘└──────────────────┘   └──┘└──────┘└┘
typ       └──────┘└──────────────────┘  └──┘└──────┘└┘
doc       └──────┘                       └──┘        └┘
txt       └──────┘                       └──┘        └┘
par       └──────┘                       └──┘        └┘
pid                                       └┘        
st     └───────────────────────────────┘└────────────┘└┘
437  
438  @[simp] lemma add_le_iff_nonpos_right : x + y ≤ x ↔ y ≤ 0 :=
id                                                  
src                                                     
typ                                                 
doc    └──┘
439  by { convert add_le_add_iff_left x, rw [add_zero] }
id                └─────────────────┘       └──────┘
src       └──────┘└─────────────────┘   └──┘└──────┘└┘
typ       └──────┘└─────────────────┘  └──┘└──────┘└┘
doc       └──────┘                      └──┘        └┘
txt       └──────┘                      └──┘        └┘
par       └──────┘                      └──┘        └┘
pid                                      └┘        
st     └──────────────────────────────┘└────────────┘└┘
440  
441  @[simp] lemma add_lt_iff_neg_right : x + y < y ↔ x < 0 :=
id                                               
src                                                  
typ                                              
doc    └──┘
442  by { convert add_lt_add_iff_right y, rw [zero_add] }
id                └──────────────────┘       └──────┘
src       └──────┘└──────────────────┘   └──┘└──────┘└┘
typ       └──────┘└──────────────────┘  └──┘└──────┘└┘
doc       └──────┘                       └──┘        └┘
txt       └──────┘                       └──┘        └┘
par       └──────┘                       └──┘        └┘
pid                                       └┘        
st     └───────────────────────────────┘└────────────┘└┘
443  
444  @[simp] lemma add_lt_iff_neg_left : x + y < x ↔ y < 0 :=
id                                              
src                                                 
typ                                             
doc    └──┘
445  by { convert add_lt_add_iff_left x, rw [add_zero] }
id                └─────────────────┘       └──────┘
src       └──────┘└─────────────────┘   └──┘└──────┘└┘
typ       └──────┘└─────────────────┘  └──┘└──────┘└┘
doc       └──────┘                      └──┘        └┘
txt       └──────┘                      └──┘        └┘
par       └──────┘                      └──┘        └┘
pid                                      └┘        
st     └──────────────────────────────┘└────────────┘└┘
446  
447  lemma add_eq_zero_iff_eq_zero_of_nonneg
448    (ha : 0 ≤ a) (hb : 0 ≤ b) : a + b = 0 ↔ a = 0 ∧ b = 0 :=
id                                          
src                                               
typ                                         
449  ⟨λ hab : a + b = 0,
id               
src                
typ              
450  by split; apply le_antisymm; try {assumption};
id                   └─────────┘
src     └───┘  └────┘└─────────┘  └───┘└────────┘
typ     └───┘  └────┘└─────────┘  └───┘└────────┘
doc     └───┘  └────┘             └───┘└────────┘
txt     └───┘  └────┘             └───┘└────────┘
par     └───┘  └────┘             └───┘└────────┘
pid                                 └───────────┘
st     └──────────────────────────────┘└────────┘└┘
451     rw ← hab; simp [ha, hb],
id           └─┘        └┘  └┘
src     └───┘     └────┘  └┘  
typ     └───┘└─┘  └────┘└┘└┘└┘
doc     └───┘     └────┘  └┘  
txt     └───┘     └────┘  └┘  
par     └───┘     └────┘  └┘  
pid       └─┘           └┘  
st   ─────────────────────────┘
452  λ ⟨ha', hb'⟩, by rw [ha', hb', add_zero]⟩
id                       └─┘  └─┘  └──────┘
src                   └──┘   └┘   └┘└──────┘
typ                  └──┘└─┘└┘└─┘└┘└──────┘
doc                   └──┘   └┘   └┘        
txt                   └──┘   └┘   └┘        
par                   └──┘   └┘   └┘        
pid                     └┘   └┘   └┘        
st                   └──────┘└───┘└────────┘
453  
454  lemma with_top.add_lt_add_iff_left :
455    ∀{a b c : with_top α}, a < ⊤ → (a + c < a + b ↔ c < b)
id              └──────┘                    
src              └──────┘                          
typ             └──────┘                    
456  | none := assume b c h, (lt_irrefl ⊤ h).elim
id     └──┘                └───────┘   └──┘
src    └──┘                   └───────┘    └──┘
typ    └──┘                └───────┘   └──┘
457  | (some a) :=
id      └──┘
src     └──┘
typ     └──┘
458    begin
st     └─────
459      assume b c h,
src      └──────────┘
typ      └──────────┘
doc      └──────────┘
txt      └──────────┘
par      └──────────┘
pid      └──────────┘
st   ───────────────┘└─
460      cases b; cases c;
id                     
src      └────┘   └────┘
typ      └────┘  └────┘
doc      └────┘   └────┘
txt      └────┘   └────┘
par      └────┘   └────┘
pid                   
st   ──────────────────────
461        simp [with_top.none_eq_top, with_top.some_eq_coe, with_top.coe_lt_top, with_top.coe_lt_coe],
id               └──────────────────┘  └──────────────────┘  └─────────────────┘  └─────────────────┘
src        └────┘└──────────────────┘└┘└──────────────────┘└┘└─────────────────┘└┘└─────────────────┘
typ        └────┘└──────────────────┘└┘└──────────────────┘└┘└─────────────────┘└┘└─────────────────┘
doc        └────┘                    └┘                    └┘                   └┘                   
txt        └────┘                    └┘                    └┘                   └┘                   
par        └────┘                    └┘                    └┘                   └┘                   
pid                                └┘                    └┘                   └┘                   
st   ────────────────────────────────────────────────────────────────────────────────────────────────┘└─
462      { rw [← with_top.coe_add], exact with_top.coe_lt_top _ },
id               └──────────────┘         └─────────────────┘
src        └────┘└──────────────┘  └────┘└─────────────────┘└─┘
typ        └────┘└──────────────┘  └────┘└─────────────────┘└─┘
doc        └────┘                  └────┘                   └─┘
txt        └────┘                  └────┘                   └─┘
par        └────┘                  └────┘                   └─┘
pid          └──┘                                          └┘
st   ─────┘└────────────────────┘└────────────────────────────┘└┘
463      { rw [← with_top.coe_add, ← with_top.coe_add, with_top.coe_lt_coe],
id               └──────────────┘    └──────────────┘  └─────────────────┘
src        └────┘└──────────────┘└──┘└──────────────┘└┘└─────────────────┘
typ        └────┘└──────────────┘└──┘└──────────────┘└┘└─────────────────┘
doc        └────┘                └──┘                └┘                   
txt        └────┘                └──┘                └┘                   
par        └────┘                └──┘                └┘                   
pid          └──┘                └──┘                └┘                   
st   ───────────────────────────┘└──────────────────┘└───────────────────┘└─
464        exact add_lt_add_iff_left _ }
id               └─────────────────┘
src        └────┘└─────────────────┘└─┘
typ        └────┘└─────────────────┘└─┘
doc        └────┘                   └─┘
txt        └────┘                   └─┘
par        └────┘                   └─┘
pid                                └┘
st   ─────────────────────────────────┘└─
465    end
st   ────┘
466  
467  lemma with_top.add_lt_add_iff_right
468    {a b c : with_top α} : a < ⊤ → (c + a < b + a ↔ c < b) :=
id              └──────┘                     
src             └──────┘                           
typ             └──────┘                     
469  by simpa [add_comm] using @with_top.add_lt_add_iff_left _ _ a b c
id             └──────┘         └──────────────────────────┘       
src     └─────┘└──────┘└──────┘ └──────────────────────────┘└───┘   
typ     └─────┘└──────┘└──────┘ └──────────────────────────┘└───┘
doc     └─────┘        └──────┘                             └───┘   
txt     └─────┘        └──────┘                             └───┘   
par     └─────┘        └──────┘                             └───┘   
pid                  └────┘                             └───┘   
st     └───────────────────────────────────────────────────────────────
470  
src  
typ  
doc  
txt  
par  
pid  
st   
471  end ordered_cancel_comm_monoid
472  
473  section ordered_comm_group
474  
475  /--
476  The `add_lt_add_left` field of `ordered_comm_group` is redundant, but it is in core so
477  we can't remove it for now. This alternative constructor is the best we can do.
478  -/
479  def ordered_comm_group.mk' {α : Type u} [add_comm_group α] [partial_order α]
id                                            └────────────┘    └───────────┘ 
src                                           └────────────┘     └───────────┘
typ                                           └────────────┘    └───────────┘ 
480    (add_le_add_left : ∀ a b : α, a ≤ b → ∀ c : α, c + a ≤ c + b) :
id                                                     
src                                                          
typ                                                    
481    ordered_comm_group α :=
id     └────────────────┘ 
src    └────────────────┘
typ    └────────────────┘ 
482  { add_le_add_left := add_le_add_left,
id                        └─────────────┘
src                       └─────────────┘
typ                       └─────────────┘
483    add_lt_add_left := λ a b h c,
id                             
typ                            
484    begin
st     └─────
485      rw lt_iff_le_not_le at h,
id          └──────────────┘
src      └─┘└──────────────┘└───┘
typ      └─┘└──────────────┘└───┘
doc      └─┘                └───┘
txt      └─┘                └───┘
par      └─┘                └───┘
pid                        └───┘
st   ───────────────────────────┘└─
486      rw lt_iff_le_not_le,
id          └──────────────┘
src      └─┘└──────────────┘
typ      └─┘└──────────────┘
doc      └─┘
txt      └─┘
par      └─┘
pid        
st   ──────────────────────┘└─
487      split,
src      └───┘
typ      └───┘
doc      └───┘
txt      └───┘
par      └───┘
st   ────────┘└─
488      { apply add_le_add_left _ _ h.1 },
id               └─────────────┘     
src        └────┘└─────────────┘└───┘ └─┘
typ        └────┘└─────────────┘└───┘└─┘
doc        └────┘               └───┘ └─┘
txt        └────┘               └───┘ └─┘
par        └────┘               └───┘ └─┘
pid                            └───┘ └─┘
st   ─────┘└────────────────────────────┘└┘
489      { intro w,
src        └─────┘
typ        └─────┘
doc        └─────┘
txt        └─────┘
par        └─────┘
pid             └┘
st   ────────────┘└─
490        replace w : -c + (c + b) ≤ -c + (c + a) := add_le_add_left _ _ w _,
id                                              └─────────────┘     
src        └──────────┘     └┘       └───┘└─────────────┘└───┘ └┘
typ        └──────────┘    └┘     └───┘└─────────────┘└───┘└┘
doc        └──────────┘       └┘        └───┘               └───┘ └┘
txt        └──────────┘       └┘        └───┘               └───┘ └┘
par        └──────────┘       └┘        └───┘               └───┘ └┘
pid               └┘└─┘       └┘        └──┘               └───┘ └┘
st   ───────────────────────────────────────────────────────────────────────┘└─
491        simp only [add_zero, add_comm, add_left_neg, add_left_comm] at w,
id                    └──────┘  └──────┘  └──────────┘  └───────────┘
src        └─────────┘└──────┘└┘└──────┘└┘└──────────┘└┘└───────────┘└────┘
typ        └─────────┘└──────┘└┘└──────┘└┘└──────────┘└┘└───────────┘└────┘
doc        └─────────┘        └┘        └┘            └┘             └────┘
txt        └─────────┘        └┘        └┘            └┘             └────┘
par        └─────────┘        └┘        └┘            └┘             └────┘
pid            └──┘└┘        └┘        └┘            └┘             └──┘
st   ─────────────────────────────────────────────────────────────────────┘└─
492        exact h.2 w },
id                  
src        └────┘ └─┘ 
typ        └────┘└─┘
doc        └────┘ └─┘ 
txt        └────┘ └─┘ 
par        └────┘ └─┘ 
pid              └─┘ 
st   ─────────────────┘└──
493    end,
st   ────┘
494    ..(by apply_instance : add_comm_group α),
id                            └────────────┘ 
src          └─────────────┘  └────────────┘
typ          └─────────────┘  └────────────┘ 
doc          └─────────────┘
txt          └─────────────┘
par          └─────────────┘
pid                        
st          └──────────────┘
495    ..(by apply_instance : partial_order α)  }
id                            └───────────┘ 
src          └─────────────┘  └───────────┘
typ          └─────────────┘  └───────────┘ 
doc          └─────────────┘
txt          └─────────────┘
par          └─────────────┘
pid                        
st          └──────────────┘
496  
497  variables [ordered_comm_group α] {a b c : α}
id              └────────────────┘
src             └────────────────┘
typ             └────────────────┘
498  
499  lemma neg_neg_iff_pos {α : Type} [_inst_1 : ordered_comm_group α] {a : α} : -a < 0 ↔ 0 < a :=
id                                               └────────────────┘                    
src                                              └────────────────┘                      
typ                                              └────────────────┘                    
500  ⟨ pos_of_neg_neg, neg_neg_of_pos ⟩
id     └────────────┘  └────────────┘
src    └────────────┘  └────────────┘
typ    └────────────┘  └────────────┘
501  
502  @[simp] lemma neg_le_neg_iff : -a ≤ -b ↔ b ≤ a :=
id                                        
src                                         
typ                                       
doc    └──┘
503  have a + b + -a ≤ a + b + -b ↔ -a ≤ -b, from add_le_add_iff_left _,
id                             └─────────────────┘
src                                    └─────────────────┘
typ                            └─────────────────┘
504  by simp at this; simp [this]
id                          └──┘
src     └──────────┘  └────┘    └─
typ     └──────────┘  └────┘└──┘└─
doc     └──────────┘  └────┘    └─
txt     └──────────┘  └────┘    └─
par     └──────────┘  └────┘    └─
pid         └─────┘          
st     └──────────────────────────
505  
src  
typ  
doc  
txt  
par  
pid  
st   
506  lemma neg_le : -a ≤ b ↔ -b ≤ a :=
id                        
src                         
typ                       
507  have -a ≤ -(-b) ↔ -b ≤ a, from neg_le_neg_iff,
id                       └────────────┘
src                          └────────────┘
typ                      └────────────┘
508  by rwa neg_neg at this
id          └─────┘
src     └──┘└─────┘└────────
typ     └──┘└─────┘└────────
doc     └──┘       └────────
txt     └──┘       └────────
par     └──┘       └────────
pid               └──────┘
st     └────────────────────
509  
src  
typ  
doc  
txt  
par  
pid  
st   
510  lemma le_neg : a ≤ -b ↔ b ≤ -a :=
id                        
src                          
typ                       
511  have -(-a) ≤ -b ↔ b ≤ -a, from neg_le_neg_iff,
id                       └────────────┘
src                          └────────────┘
typ                      └────────────┘
512  by rwa neg_neg at this
id          └─────┘
src     └──┘└─────┘└────────
typ     └──┘└─────┘└────────
doc     └──┘       └────────
txt     └──┘       └────────
par     └──┘       └────────
pid               └──────┘
st     └────────────────────
513  
src  
typ  
doc  
txt  
par  
pid  
st   
514  lemma neg_le_iff_add_nonneg : -a ≤ b ↔ 0 ≤ a + b :=
id                                          
src                                           
typ                                         
515  (add_le_add_iff_left a).symm.trans $ by rw add_neg_self
id    └─────────────────┘  └──┘ └───┘          └──────────┘
src   └─────────────────┘   └──┘ └───┘       └─┘└──────────┘
typ   └─────────────────┘  └──┘ └───┘       └─┘└──────────┘
doc                                          └─┘            
txt                                          └─┘            
par                                          └─┘            
pid                                                        
st                                          └────────────────
516  
src  
typ  
doc  
txt  
par  
pid  
st   
517  lemma le_neg_iff_add_nonpos : a ≤ -b ↔ a + b ≤ 0 :=
id                                        
src                                           
typ                                       
518  (add_le_add_iff_right b).symm.trans $ by rw neg_add_self
id    └──────────────────┘  └──┘ └───┘          └──────────┘
src   └──────────────────┘   └──┘ └───┘       └─┘└──────────┘
typ   └──────────────────┘  └──┘ └───┘       └─┘└──────────┘
doc                                           └─┘            
txt                                           └─┘            
par                                           └─┘            
pid                                                         
st                                           └────────────────
519  
src  
typ  
doc  
txt  
par  
pid  
st   
520  @[simp] lemma neg_nonpos : -a ≤ 0 ↔ 0 ≤ a :=
id                                      
src                                     
typ                                     
doc    └──┘
521  have -a ≤ -0 ↔ 0 ≤ a, from neg_le_neg_iff,
id                       └────────────┘
src                        └────────────┘
typ                      └────────────┘
522  by rwa neg_zero at this
id          └──────┘
src     └──┘└──────┘└────────
typ     └──┘└──────┘└────────
doc     └──┘        └────────
txt     └──┘        └────────
par     └──┘        └────────
pid                └──────┘
st     └─────────────────────
523  
src  
typ  
doc  
txt  
par  
pid  
st   
524  @[simp] lemma neg_nonneg : 0 ≤ -a ↔ a ≤ 0 :=
id                                    
src                                     
typ                                   
doc    └──┘
525  have -0 ≤ -a ↔ a ≤ 0, from neg_le_neg_iff,
id                       └────────────┘
src                        └────────────┘
typ                      └────────────┘
526  by rwa neg_zero at this
id          └──────┘
src     └──┘└──────┘└────────
typ     └──┘└──────┘└────────
doc     └──┘        └────────
txt     └──┘        └────────
par     └──┘        └────────
pid                └──────┘
st     └─────────────────────
527  
src  
typ  
doc  
txt  
par  
pid  
st   
528  lemma neg_le_self (h : 0 ≤ a) : -a ≤ a :=
id                                   
src                                   
typ                                  
529  le_trans (neg_nonpos.2 h) h
id   └──────┘  └────────┘    
src  └──────┘  └────────┘
typ  └──────┘  └────────┘    
530  
531  lemma self_le_neg (h : a ≤ 0) : a ≤ -a :=
id                                   
src                                    
typ                                  
532  le_trans h (neg_nonneg.2 h)
id   └──────┘   └────────┘  
src  └──────┘    └────────┘
typ  └──────┘   └────────┘  
533  
534  @[simp] lemma neg_lt_neg_iff : -a < -b ↔ b < a :=
id                                        
src                                         
typ                                       
doc    └──┘
535  have a + b + -a < a + b + -b ↔ -a < -b, from add_lt_add_iff_left _,
id                             └─────────────────┘
src                                    └─────────────────┘
typ                            └─────────────────┘
536  by simp at this; simp [this]
id                          └──┘
src     └──────────┘  └────┘    └─
typ     └──────────┘  └────┘└──┘└─
doc     └──────────┘  └────┘    └─
txt     └──────────┘  └────┘    └─
par     └──────────┘  └────┘    └─
pid         └─────┘          
st     └──────────────────────────
537  
src  
typ  
doc  
txt  
par  
pid  
st   
538  lemma neg_lt_zero : -a < 0 ↔ 0 < a :=
id                               
src                              
typ                              
539  have -a < -0 ↔ 0 < a, from neg_lt_neg_iff,
id                       └────────────┘
src                        └────────────┘
typ                      └────────────┘
540  by rwa neg_zero at this
id          └──────┘
src     └──┘└──────┘└────────
typ     └──┘└──────┘└────────
doc     └──┘        └────────
txt     └──┘        └────────
par     └──┘        └────────
pid                └──────┘
st     └─────────────────────
541  
src  
typ  
doc  
txt  
par  
pid  
st   
542  lemma neg_pos : 0 < -a ↔ a < 0 :=
id                         
src                          
typ                        
543  have -0 < -a ↔ a < 0, from neg_lt_neg_iff,
id                       └────────────┘
src                        └────────────┘
typ                      └────────────┘
544  by rwa neg_zero at this
id          └──────┘
src     └──┘└──────┘└────────
typ     └──┘└──────┘└────────
doc     └──┘        └────────
txt     └──┘        └────────
par     └──┘        └────────
pid                └──────┘
st     └─────────────────────
545  
src  
typ  
doc  
txt  
par  
pid  
st   
546  lemma neg_lt : -a < b ↔ -b < a :=
id                        
src                         
typ                       
547  have -a < -(-b) ↔ -b < a, from neg_lt_neg_iff,
id                       └────────────┘
src                          └────────────┘
typ                      └────────────┘
548  by rwa neg_neg at this
id          └─────┘
src     └──┘└─────┘└────────
typ     └──┘└─────┘└────────
doc     └──┘       └────────
txt     └──┘       └────────
par     └──┘       └────────
pid               └──────┘
st     └────────────────────
549  
src  
typ  
doc  
txt  
par  
pid  
st   
550  lemma lt_neg : a < -b ↔ b < -a :=
id                        
src                          
typ                       
551  have -(-a) < -b ↔ b < -a, from neg_lt_neg_iff,
id                       └────────────┘
src                          └────────────┘
typ                      └────────────┘
552  by rwa neg_neg at this
id          └─────┘
src     └──┘└─────┘└────────
typ     └──┘└─────┘└────────
doc     └──┘       └────────
txt     └──┘       └────────
par     └──┘       └────────
pid               └──────┘
st     └────────────────────
553  
src  
typ  
doc  
txt  
par  
pid  
st   
554  lemma sub_le_sub_iff_left (a : α) {b c : α} : a - b ≤ a - c ↔ c ≤ b :=
id                                                         
src                                                              
typ                                                        
555  (add_le_add_iff_left _).trans neg_le_neg_iff
id    └─────────────────┘   └───┘  └────────────┘
src   └─────────────────┘   └───┘  └────────────┘
typ   └─────────────────┘   └───┘  └────────────┘
556  
557  lemma sub_le_sub_iff_right (c : α) : a - c ≤ b - c ↔ a ≤ b :=
id                                                 
src                                                     
typ                                                
558  add_le_add_iff_right _
id   └──────────────────┘
src  └──────────────────┘
typ  └──────────────────┘
559  
560  lemma sub_lt_sub_iff_left (a : α) {b c : α} : a - b < a - c ↔ c < b :=
id                                                         
src                                                              
typ                                                        
561  (add_lt_add_iff_left _).trans neg_lt_neg_iff
id    └─────────────────┘   └───┘  └────────────┘
src   └─────────────────┘   └───┘  └────────────┘
typ   └─────────────────┘   └───┘  └────────────┘
562  
563  lemma sub_lt_sub_iff_right (c : α) : a - c < b - c ↔ a < b :=
id                                                 
src                                                     
typ                                                
564  add_lt_add_iff_right _
id   └──────────────────┘
src  └──────────────────┘
typ  └──────────────────┘
565  
566  @[simp] lemma sub_nonneg : 0 ≤ a - b ↔ b ≤ a :=
id                                       
src                                        
typ                                      
doc    └──┘
567  have a - a ≤ a - b ↔ b ≤ a, from sub_le_sub_iff_left a,
id                         └─────────────────┘ 
src                              └─────────────────┘
typ                        └─────────────────┘ 
568  by rwa sub_self at this
id          └──────┘
src     └──┘└──────┘└────────
typ     └──┘└──────┘└────────
doc     └──┘        └────────
txt     └──┘        └────────
par     └──┘        └────────
pid                └──────┘
st     └─────────────────────
569  
src  
typ  
doc  
txt  
par  
pid  
st   
570  @[simp] lemma sub_nonpos : a - b ≤ 0 ↔ a ≤ b :=
id                                       
src                                        
typ                                      
doc    └──┘
571  have a - b ≤ b - b ↔ a ≤ b, from sub_le_sub_iff_right b,
id                         └──────────────────┘ 
src                              └──────────────────┘
typ                        └──────────────────┘ 
572  by rwa sub_self at this
id          └──────┘
src     └──┘└──────┘└────────
typ     └──┘└──────┘└────────
doc     └──┘        └────────
txt     └──┘        └────────
par     └──┘        └────────
pid                └──────┘
st     └─────────────────────
573  
src  
typ  
doc  
txt  
par  
pid  
st   
574  @[simp] lemma sub_pos : 0 < a - b ↔ b < a :=
id                                    
src                                     
typ                                   
doc    └──┘
575  have a - a < a - b ↔ b < a, from sub_lt_sub_iff_left a,
id                         └─────────────────┘ 
src                              └─────────────────┘
typ                        └─────────────────┘ 
576  by rwa sub_self at this
id          └──────┘
src     └──┘└──────┘└────────
typ     └──┘└──────┘└────────
doc     └──┘        └────────
txt     └──┘        └────────
par     └──┘        └────────
pid                └──────┘
st     └─────────────────────
577  
src  
typ  
doc  
txt  
par  
pid  
st   
578  @[simp] lemma sub_lt_zero : a - b < 0 ↔ a < b :=
id                                        
src                                         
typ                                       
doc    └──┘
579  have a - b < b - b ↔ a < b, from sub_lt_sub_iff_right b,
id                         └──────────────────┘ 
src                              └──────────────────┘
typ                        └──────────────────┘ 
580  by rwa sub_self at this
id          └──────┘
src     └──┘└──────┘└────────
typ     └──┘└──────┘└────────
doc     └──┘        └────────
txt     └──┘        └────────
par     └──┘        └────────
pid                └──────┘
st     └─────────────────────
581  
src  
typ  
doc  
txt  
par  
pid  
st   
582  lemma le_neg_add_iff_add_le : b ≤ -a + c ↔ a + b ≤ c :=
id                                           
src                                              
typ                                          
583  have -a + (a + b) ≤ -a + c ↔ a + b ≤ c, from add_le_add_iff_left _,
id                               └─────────────────┘
src                                      └─────────────────┘
typ                              └─────────────────┘
584  by rwa neg_add_cancel_left at this
id          └─────────────────┘
src     └──┘└─────────────────┘└────────
typ     └──┘└─────────────────┘└────────
doc     └──┘                   └────────
txt     └──┘                   └────────
par     └──┘                   └────────
pid                           └──────┘
st     └────────────────────────────────
585  
src  
typ  
doc  
txt  
par  
pid  
st   
586  lemma le_sub_iff_add_le' : b ≤ c - a ↔ a + b ≤ c :=
id                                        
src                                           
typ                                       
587  by rw [sub_eq_add_neg, add_comm, le_neg_add_iff_add_le]
id          └────────────┘  └──────┘  └───────────────────┘
src     └──┘└────────────┘└┘└──────┘└┘└───────────────────┘└─
typ     └──┘└────────────┘└┘└──────┘└┘└───────────────────┘└─
doc     └──┘              └┘        └┘                     └─
txt     └──┘              └┘        └┘                     └─
par     └──┘              └┘        └┘                     └─
pid       └┘              └┘        └┘                     
st     └─────────────────┘└────────┘└─────────────────────┘
588  
src  
typ  
doc  
txt  
par  
pid  
st   
589  lemma le_sub_iff_add_le : a ≤ c - b ↔ a + b ≤ c :=
id                                       
src                                          
typ                                      
590  by rw [le_sub_iff_add_le', add_comm]
id          └────────────────┘  └──────┘
src     └──┘└────────────────┘└┘└──────┘└─
typ     └──┘└────────────────┘└┘└──────┘└─
doc     └──┘                  └┘        └─
txt     └──┘                  └┘        └─
par     └──┘                  └┘        └─
pid       └┘                  └┘        
st     └─────────────────────┘└────────┘
591  
src  
typ  
doc  
txt  
par  
pid  
st   
592  @[simp] lemma neg_add_le_iff_le_add : -b + a ≤ c ↔ a ≤ b + c :=
id                                                   
src                                                      
typ                                                  
doc    └──┘
593  have -b + a ≤ -b + (b + c) ↔ a ≤ b + c, from add_le_add_iff_left _,
id                               └─────────────────┘
src                                      └─────────────────┘
typ                              └─────────────────┘
594  by rwa neg_add_cancel_left at this
id          └─────────────────┘
src     └──┘└─────────────────┘└────────
typ     └──┘└─────────────────┘└────────
doc     └──┘                   └────────
txt     └──┘                   └────────
par     └──┘                   └────────
pid                           └──────┘
st     └────────────────────────────────
595  
src  
typ  
doc  
txt  
par  
pid  
st   
596  lemma sub_le_iff_le_add' : a - b ≤ c ↔ a ≤ b + c :=
id                                        
src                                           
typ                                       
597  by rw [sub_eq_add_neg, add_comm, neg_add_le_iff_le_add]
id          └────────────┘  └──────┘  └───────────────────┘
src     └──┘└────────────┘└┘└──────┘└┘└───────────────────┘└─
typ     └──┘└────────────┘└┘└──────┘└┘└───────────────────┘└─
doc     └──┘              └┘        └┘                     └─
txt     └──┘              └┘        └┘                     └─
par     └──┘              └┘        └┘                     └─
pid       └┘              └┘        └┘                     
st     └─────────────────┘└────────┘└─────────────────────┘
598  
src  
typ  
doc  
txt  
par  
pid  
st   
599  lemma sub_le_iff_le_add : a - c ≤ b ↔ a ≤ b + c :=
id                                       
src                                          
typ                                      
600  by rw [sub_le_iff_le_add', add_comm]
id          └────────────────┘  └──────┘
src     └──┘└────────────────┘└┘└──────┘└─
typ     └──┘└────────────────┘└┘└──────┘└─
doc     └──┘                  └┘        └─
txt     └──┘                  └┘        └─
par     └──┘                  └┘        └─
pid       └┘                  └┘        
st     └─────────────────────┘└────────┘
601  
src  
typ  
doc  
txt  
par  
pid  
st   
602  @[simp] lemma add_neg_le_iff_le_add : a + -c ≤ b ↔ a ≤ b + c :=
id                                                   
src                                                      
typ                                                  
doc    └──┘
603  sub_le_iff_le_add
id   └───────────────┘
src  └───────────────┘
typ  └───────────────┘
604  
605  @[simp] lemma add_neg_le_iff_le_add' : a + -b ≤ c ↔ a ≤ b + c :=
id                                                    
src                                                       
typ                                                   
doc    └──┘
606  sub_le_iff_le_add'
id   └────────────────┘
src  └────────────────┘
typ  └────────────────┘
607  
608  lemma neg_add_le_iff_le_add' : -c + a ≤ b ↔ a ≤ b + c :=
id                                            
src                                               
typ                                           
609  by rw [neg_add_le_iff_le_add, add_comm]
id          └───────────────────┘  └──────┘
src     └──┘└───────────────────┘└┘└──────┘└─
typ     └──┘└───────────────────┘└┘└──────┘└─
doc     └──┘                     └┘        └─
txt     └──┘                     └┘        └─
par     └──┘                     └┘        └─
pid       └┘                     └┘        
st     └────────────────────────┘└────────┘
610  
src  
typ  
doc  
txt  
par  
pid  
st   
611  @[simp] lemma neg_le_sub_iff_le_add : -b ≤ a - c ↔ c ≤ a + b :=
id                                                   
src                                                      
typ                                                  
doc    └──┘
612  le_sub_iff_add_le.trans neg_add_le_iff_le_add'
id   └───────────────┘└────┘ └────────────────────┘
src  └───────────────┘└────┘ └────────────────────┘
typ  └───────────────┘└────┘ └────────────────────┘
613  
614  lemma neg_le_sub_iff_le_add' : -a ≤ b - c ↔ c ≤ a + b :=
id                                            
src                                               
typ                                           
615  by rw [neg_le_sub_iff_le_add, add_comm]
id          └───────────────────┘  └──────┘
src     └──┘└───────────────────┘└┘└──────┘└─
typ     └──┘└───────────────────┘└┘└──────┘└─
doc     └──┘                     └┘        └─
txt     └──┘                     └┘        └─
par     └──┘                     └┘        └─
pid       └┘                     └┘        
st     └────────────────────────┘└────────┘
616  
src  
typ  
doc  
txt  
par  
pid  
st   
617  lemma sub_le : a - b ≤ c ↔ a - c ≤ b :=
id                            
src                               
typ                           
618  sub_le_iff_le_add'.trans sub_le_iff_le_add.symm
id   └────────────────┘└────┘ └───────────────┘└───┘
src  └────────────────┘└────┘ └───────────────┘└───┘
typ  └────────────────┘└────┘ └───────────────┘└───┘
619  
620  theorem le_sub : a ≤ b - c ↔ c ≤ b - a :=
id                              
src                                 
typ                             
621  le_sub_iff_add_le'.trans le_sub_iff_add_le.symm
id   └────────────────┘└────┘ └───────────────┘└───┘
src  └────────────────┘└────┘ └───────────────┘└───┘
typ  └────────────────┘└────┘ └───────────────┘└───┘
622  
623  @[simp] lemma lt_neg_add_iff_add_lt : b < -a + c ↔ a + b < c :=
id                                                   
src                                                      
typ                                                  
doc    └──┘
624  have -a + (a + b) < -a + c ↔ a + b < c, from add_lt_add_iff_left _,
id                               └─────────────────┘
src                                      └─────────────────┘
typ                              └─────────────────┘
625  by rwa neg_add_cancel_left at this
id          └─────────────────┘
src     └──┘└─────────────────┘└────────
typ     └──┘└─────────────────┘└────────
doc     └──┘                   └────────
txt     └──┘                   └────────
par     └──┘                   └────────
pid                           └──────┘
st     └────────────────────────────────
626  
src  
typ  
doc  
txt  
par  
pid  
st   
627  lemma lt_sub_iff_add_lt' : b < c - a ↔ a + b < c :=
id                                        
src                                           
typ                                       
628  by rw [sub_eq_add_neg, add_comm, lt_neg_add_iff_add_lt]
id          └────────────┘  └──────┘  └───────────────────┘
src     └──┘└────────────┘└┘└──────┘└┘└───────────────────┘└─
typ     └──┘└────────────┘└┘└──────┘└┘└───────────────────┘└─
doc     └──┘              └┘        └┘                     └─
txt     └──┘              └┘        └┘                     └─
par     └──┘              └┘        └┘                     └─
pid       └┘              └┘        └┘                     
st     └─────────────────┘└────────┘└─────────────────────┘
629  
src  
typ  
doc  
txt  
par  
pid  
st   
630  lemma lt_sub_iff_add_lt : a < c - b ↔ a + b < c :=
id                                       
src                                          
typ                                      
631  by rw [lt_sub_iff_add_lt', add_comm]
id          └────────────────┘  └──────┘
src     └──┘└────────────────┘└┘└──────┘└─
typ     └──┘└────────────────┘└┘└──────┘└─
doc     └──┘                  └┘        └─
txt     └──┘                  └┘        └─
par     └──┘                  └┘        └─
pid       └┘                  └┘        
st     └─────────────────────┘└────────┘
632  
src  
typ  
doc  
txt  
par  
pid  
st   
633  @[simp] lemma neg_add_lt_iff_lt_add : -b + a < c ↔ a < b + c :=
id                                                   
src                                                      
typ                                                  
doc    └──┘
634  have -b + a < -b + (b + c) ↔ a < b + c, from add_lt_add_iff_left _,
id                               └─────────────────┘
src                                      └─────────────────┘
typ                              └─────────────────┘
635  by rwa neg_add_cancel_left at this
id          └─────────────────┘
src     └──┘└─────────────────┘└────────
typ     └──┘└─────────────────┘└────────
doc     └──┘                   └────────
txt     └──┘                   └────────
par     └──┘                   └────────
pid                           └──────┘
st     └────────────────────────────────
636  
src  
typ  
doc  
txt  
par  
pid  
st   
637  lemma sub_lt_iff_lt_add' : a - b < c ↔ a < b + c :=
id                                        
src                                           
typ                                       
638  by rw [sub_eq_add_neg, add_comm, neg_add_lt_iff_lt_add]
id          └────────────┘  └──────┘  └───────────────────┘
src     └──┘└────────────┘└┘└──────┘└┘└───────────────────┘└─
typ     └──┘└────────────┘└┘└──────┘└┘└───────────────────┘└─
doc     └──┘              └┘        └┘                     └─
txt     └──┘              └┘        └┘                     └─
par     └──┘              └┘        └┘                     └─
pid       └┘              └┘        └┘                     
st     └─────────────────┘└────────┘└─────────────────────┘
639  
src  
typ  
doc  
txt  
par  
pid  
st   
640  lemma sub_lt_iff_lt_add : a - c < b ↔ a < b + c :=
id                                       
src                                          
typ                                      
641  by rw [sub_lt_iff_lt_add', add_comm]
id          └────────────────┘  └──────┘
src     └──┘└────────────────┘└┘└──────┘└─
typ     └──┘└────────────────┘└┘└──────┘└─
doc     └──┘                  └┘        └─
txt     └──┘                  └┘        └─
par     └──┘                  └┘        └─
pid       └┘                  └┘        
st     └─────────────────────┘└────────┘
642  
src  
typ  
doc  
txt  
par  
pid  
st   
643  lemma neg_add_lt_iff_lt_add_right : -c + a < b ↔ a < b + c :=
id                                                 
src                                                    
typ                                                
644  by rw [neg_add_lt_iff_lt_add, add_comm]
id          └───────────────────┘  └──────┘
src     └──┘└───────────────────┘└┘└──────┘└─
typ     └──┘└───────────────────┘└┘└──────┘└─
doc     └──┘                     └┘        └─
txt     └──┘                     └┘        └─
par     └──┘                     └┘        └─
pid       └┘                     └┘        
st     └────────────────────────┘└────────┘
645  
src  
typ  
doc  
txt  
par  
pid  
st   
646  @[simp] lemma neg_lt_sub_iff_lt_add : -b < a - c ↔ c < a + b :=
id                                                   
src                                                      
typ                                                  
doc    └──┘
647  lt_sub_iff_add_lt.trans neg_add_lt_iff_lt_add_right
id   └───────────────┘└────┘ └─────────────────────────┘
src  └───────────────┘└────┘ └─────────────────────────┘
typ  └───────────────┘└────┘ └─────────────────────────┘
648  
649  lemma neg_lt_sub_iff_lt_add' : -a < b - c ↔ c < a + b :=
id                                            
src                                               
typ                                           
650  by rw [neg_lt_sub_iff_lt_add, add_comm]
id          └───────────────────┘  └──────┘
src     └──┘└───────────────────┘└┘└──────┘└─
typ     └──┘└───────────────────┘└┘└──────┘└─
doc     └──┘                     └┘        └─
txt     └──┘                     └┘        └─
par     └──┘                     └┘        └─
pid       └┘                     └┘        
st     └────────────────────────┘└────────┘
651  
src  
typ  
doc  
txt  
par  
pid  
st   
652  lemma sub_lt : a - b < c ↔ a - c < b :=
id                            
src                               
typ                           
653  sub_lt_iff_lt_add'.trans sub_lt_iff_lt_add.symm
id   └────────────────┘└────┘ └───────────────┘└───┘
src  └────────────────┘└────┘ └───────────────┘└───┘
typ  └────────────────┘└────┘ └───────────────┘└───┘
654  
655  theorem lt_sub : a < b - c ↔ c < b - a :=
id                              
src                                 
typ                             
656  lt_sub_iff_add_lt'.trans lt_sub_iff_add_lt.symm
id   └────────────────┘└────┘ └───────────────┘└───┘
src  └────────────────┘└────┘ └───────────────┘└───┘
typ  └────────────────┘└────┘ └───────────────┘└───┘
657  
658  lemma sub_le_self_iff (a : α) {b : α} : a - b ≤ a ↔ 0 ≤ b :=
id                                                  
src                                                     
typ                                                 
659  sub_le_iff_le_add'.trans (le_add_iff_nonneg_left _)
id   └────────────────┘└────┘  └────────────────────┘
src  └────────────────┘└────┘  └────────────────────┘
typ  └────────────────┘└────┘  └────────────────────┘
660  
661  lemma sub_lt_self_iff (a : α) {b : α} : a - b < a ↔ 0 < b :=
id                                                  
src                                                     
typ                                                 
662  sub_lt_iff_lt_add'.trans (lt_add_iff_pos_left _)
id   └────────────────┘└────┘  └─────────────────┘
src  └────────────────┘└────┘  └─────────────────┘
typ  └────────────────┘└────┘  └─────────────────┘
663  
664  end ordered_comm_group
665  
666  namespace decidable_linear_ordered_comm_group
667  variables [s : decidable_linear_ordered_comm_group α]
id                  └─────────────────────────────────┘
src                 └─────────────────────────────────┘
typ                 └─────────────────────────────────┘
668  include s
669  
670  @[priority 100] -- see Note [lower instance priority]
671  instance : decidable_linear_ordered_cancel_comm_monoid α :=
id              └─────────────────────────────────────────┘ 
src             └─────────────────────────────────────────┘
typ             └─────────────────────────────────────────┘ 
672  { le_of_add_le_add_left := λ x y z, le_of_add_le_add_left,
id                                    └───────────────────┘
src                                      └───────────────────┘
typ                                   └───────────────────┘
673    add_left_cancel := λ x y z, add_left_cancel,
id                              └─────────────┘
src                                └─────────────┘
typ                             └─────────────┘
674    add_right_cancel := λ x y z, add_right_cancel,
id                               └──────────────┘
src                                 └──────────────┘
typ                              └──────────────┘
675    ..s }
id       
typ      
676  
677  lemma eq_of_abs_sub_nonpos {a b : α} (h : abs (a - b) ≤ 0) : a = b :=
id                                            └─┘              
src                                            └─┘                
typ                                           └─┘              
678  eq_of_abs_sub_eq_zero (le_antisymm _ _ h (abs_nonneg (a - b)))
id   └───────────────────┘  └─────────┘       └────────┘    
src  └───────────────────┘  └─────────┘        └────────┘    
typ  └───────────────────┘  └─────────┘       └────────┘    
679  
680  end decidable_linear_ordered_comm_group
681  
682  set_option old_structure_cmd true
doc             └───────────────┘
683  section prio
684  set_option default_priority 100 -- see Note [default priority]
doc             └──────────────┘
685  /-- This is not so much a new structure as a construction mechanism
686    for ordered groups, by specifying only the "positive cone" of the group. -/
687  class nonneg_comm_group (α : Type*) extends add_comm_group α :=
id                               └───┘          └────────────┘ 
src                                              └────────────┘
typ                              └───┘          └────────────┘ 
688  (nonneg : α → Prop)
id              
typ             
689  (pos : α → Prop := λ a, nonneg a ∧ ¬ nonneg (neg a))
id                        └────┘    └────┘  └─┘ 
src                                   
typ                       └────┘    └────┘  └─┘ 
690  (pos_iff : ∀ a, pos a ↔ nonneg a ∧ ¬ nonneg (-a) . order_laws_tac)
id                  └─┘   └────┘    └────┘  
src                 └─┘                       
typ                 └─┘   └────┘    └────┘  
doc               
691  (zero_nonneg : nonneg 0)
id                  └────┘
typ                 └────┘
692  (add_nonneg : ∀ {a b}, nonneg a → nonneg b → nonneg (a + b))
id                       └────┘    └────┘    └────┘    
src                                                        
typ                      └────┘    └────┘    └────┘    
693  (nonneg_antisymm : ∀ {a}, nonneg a → nonneg (-a) → a = 0)
id                           └────┘    └────┘       
src                                                      
typ                          └────┘    └────┘       
694  end prio
695  
696  namespace nonneg_comm_group
697  variable [s : nonneg_comm_group α]
id                 └───────────────┘
src                └───────────────┘
typ                └───────────────┘
doc                └───────────────┘
698  include s
699  
700  @[reducible, priority 100] -- see Note [lower instance priority]
doc    └───────┘
701  instance to_ordered_comm_group : ordered_comm_group α :=
id                                    └────────────────┘ 
src                                   └────────────────┘
typ                                   └────────────────┘ 
702  { le := λ a b, nonneg (b - a),
id                └────┘    
src                 └────┘    
typ               └────┘    
703    lt := λ a b, pos (b - a),
id                └─┘    
src                 └─┘    
typ               └─┘    
704    lt_iff_le_not_le := λ a b, by simp; rw [pos_iff]; simp,
id                                           └─────┘
src                                  └──┘  └──┘└─────┘  └──┘
typ                                └──┘  └──┘└─────┘  └──┘
doc                                  └──┘  └──┘         └──┘
txt                                  └──┘  └──┘         └──┘
par                                  └──┘  └──┘         └──┘
pid                                          └┘       
st                                  └─────────┘└─────┘└────┘
705    le_refl := λ a, by simp [zero_nonneg],
id                             └─────────┘
src                       └────┘└─────────┘
typ                      └────┘└─────────┘
doc                       └────┘           
txt                       └────┘           
par                       └────┘           
pid                                      
st                       └─────────────────┘
706    le_trans := λ a b c nab nbc, by simp [-sub_eq_add_neg];
id                      └─┘ └─┘
src                                    └────────────────────┘
typ                     └─┘ └─┘     └────────────────────┘
doc                                    └────────────────────┘
txt                                    └────────────────────┘
par                                    └────────────────────┘
pid                                        └───────────────┘
st                                    └────────────────────────
707      rw ← sub_add_sub_cancel; exact add_nonneg nbc nab,
id            └────────────────┘        └────────┘ └─┘ └─┘
src      └───┘└────────────────┘  └────┘└────────┘   
typ      └───┘└────────────────┘  └────┘└────────┘└─┘└─┘
doc      └───┘                    └────┘             
txt      └───┘                    └────┘             
par      └───┘                    └────┘             
pid        └─┘                                      
st   ────────────────────────────────────────────────────┘
708    le_antisymm := λ a b nab nba, eq_of_sub_eq_zero $
id                        └─┘ └─┘  └───────────────┘
src                                  └───────────────┘
typ                       └─┘ └─┘  └───────────────┘
709      nonneg_antisymm nba (by rw neg_sub; exact nab),
id       └─────────────┘ └─┘        └─────┘        └─┘
src      └─────────────┘         └─┘└─────┘  └────┘
typ      └─────────────┘ └─┘     └─┘└─────┘  └────┘└─┘
doc                              └─┘         └────┘
txt                              └─┘         └────┘
par                              └─┘         └────┘
pid                                              
st                              └────────────────────┘
710    add_le_add_left := λ a b nab c, by simpa [(≤), preorder.le] using nab,
id                            └─┘                                     └─┘
src                                       └─────┘ └──┘           └──────┘
typ                           └─┘      └─────┘ └──┘           └──────┘└─┘
doc                                       └─────┘ └──┘           └──────┘
txt                                       └─────┘ └──┘           └──────┘
par                                       └─────┘ └──┘           └──────┘
pid                                             └──┘           └────┘
st                                       └─────────────────────────────────┘
711    add_lt_add_left := λ a b nab c, by simpa [(<), preorder.lt] using nab, ..s }
id                            └─┘                                     └─┘    
src                                       └─────┘ └──┘           └──────┘
typ                           └─┘      └─────┘ └──┘           └──────┘└─┘    
doc                                       └─────┘ └──┘           └──────┘
txt                                       └─────┘ └──┘           └──────┘
par                                       └─────┘ └──┘           └──────┘
pid                                             └──┘           └────┘
st                                       └─────────────────────────────────┘
712  
713  theorem nonneg_def {a : α} : nonneg a ↔ 0 ≤ a :=
id                               └────┘      
src                               └────┘      
typ                              └────┘      
714  show _ ↔ nonneg _, by simp
id           └────┘
src          └────┘       └────
typ          └────┘       └────
doc                        └────
txt                        └────
par                        └────
pid                            
st                        └─────
715  
src  
typ  
doc  
txt  
par  
pid  
st   
716  theorem pos_def {a : α} : pos a ↔ 0 < a :=
id                            └─┘      
src                            └─┘      
typ                           └─┘      
717  show _ ↔ pos _, by simp
id           └─┘
src          └─┘       └────
typ          └─┘       └────
doc                     └────
txt                     └────
par                     └────
pid                         
st                     └─────
718  
src  
typ  
doc  
txt  
par  
pid  
st   
719  theorem not_zero_pos : ¬ pos (0 : α) :=
id                           └─┘      
src                          └─┘
typ                          └─┘      
720  mt pos_def.1 (lt_irrefl _)
id   └┘ └─────┘   └───────┘
src  └┘ └─────┘   └───────┘
typ  └┘ └─────┘   └───────┘
721  
722  theorem zero_lt_iff_nonneg_nonneg {a : α} :
id                                          
typ                                         
723    0 < a ↔ nonneg a ∧ ¬ nonneg (-a) :=
id          └────┘    └────┘  
src          └────┘     └────┘  
typ         └────┘    └────┘  
724  pos_def.symm.trans (pos_iff α _)
id   └─────┘└───┘└────┘  └─────┘ 
src  └─────┘└───┘└────┘  └─────┘
typ  └─────┘└───┘└────┘  └─────┘ 
725  
726  theorem nonneg_total_iff :
727    (∀ a : α, nonneg a ∨ nonneg (-a)) ↔
id              └────┘   └────┘     
src              └────┘    └────┘      
typ             └────┘   └────┘     
728    (∀ a b : α, a ≤ b ∨ b ≤ a) :=
id                      
src                        
typ                     
729  ⟨λ h a b, by have := h (b - a); rwa [neg_sub] at this,
id                                 └─────┘
src               └──────┘      └───┘└─────┘└───────┘
typ            └──────┘   └───┘└─────┘└───────┘
doc               └──────┘       └───┘       └───────┘
txt               └──────┘       └───┘       └───────┘
par               └──────┘       └───┘       └───────┘
pid               └───┘└─┘          └┘       └──────┘
st               └───────────────────────┘└─────┘└──────┘
730   λ h a, by rw [nonneg_def, nonneg_def, neg_nonneg]; apply h⟩
id                └────────┘  └────────┘  └────────┘
src             └──┘└────────┘└┘└────────┘└┘└────────┘  └────┘
typ           └──┘└────────┘└┘└────────┘└┘└────────┘  └────┘
doc             └──┘          └┘          └┘            └────┘
txt             └──┘          └┘          └┘            └────┘
par             └──┘          └┘          └┘            └────┘
pid               └┘          └┘          └┘                 
st             └─────────────┘└──────────┘└──────────┘└───────┘
731  
732  def to_decidable_linear_ordered_comm_group
733    [decidable_pred (@nonneg α _)]
id      └────────────┘   └────┘ 
src     └────────────┘   └────┘
typ     └────────────┘   └────┘ 
734    (nonneg_total : ∀ a : α, nonneg a ∨ nonneg (-a))
id                             └────┘   └────┘  
src                             └────┘    └────┘  
typ                            └────┘   └────┘  
735    : decidable_linear_ordered_comm_group α :=
id       └─────────────────────────────────┘ 
src      └─────────────────────────────────┘
typ      └─────────────────────────────────┘ 
736  { le := (≤),
id           
src          
typ          
737    lt := (<),
id           
src          
typ          
738    lt_iff_le_not_le := @lt_iff_le_not_le _ _,
id                          └──────────────┘
src                         └──────────────┘
typ                         └──────────────┘
739    le_refl := @le_refl _ _,
id                 └─────┘
src                └─────┘
typ                └─────┘
740    le_trans := @le_trans _ _,
id                  └──────┘
src                 └──────┘
typ                 └──────┘
st                             
741    le_antisymm := @le_antisymm _ _,
id                     └─────────┘
src                    └─────────┘
typ                    └─────────┘
742    le_total := nonneg_total_iff.1 nonneg_total,
id                 └──────────────┘  └──────────┘
src                └──────────────┘
typ                └──────────────┘  └──────────┘
743    decidable_le := by apply_instance,
src                       └────────────┘
typ                       └────────────┘
doc                       └────────────┘
txt                       └────────────┘
par                       └────────────┘
st                       └─────────────┘
744    decidable_eq := by apply_instance,
src                       └────────────┘
typ                       └────────────┘
doc                       └────────────┘
txt                       └────────────┘
par                       └────────────┘
st                       └─────────────┘
745    decidable_lt := by apply_instance,
src                       └────────────┘
typ                       └────────────┘
doc                       └────────────┘
txt                       └────────────┘
par                       └────────────┘
st                       └─────────────┘
746    ..@nonneg_comm_group.to_ordered_comm_group _ s }
id        └─────────────────────────────────────┘   
src       └─────────────────────────────────────┘
typ       └─────────────────────────────────────┘   
747  
748  end nonneg_comm_group
749  
750  namespace order_dual
751  
752  instance [ordered_comm_monoid α] : ordered_comm_monoid (order_dual α) :=
id             └─────────────────┘     └─────────────────┘  └────────┘ 
src            └─────────────────┘      └─────────────────┘  └────────┘
typ            └─────────────────┘     └─────────────────┘  └────────┘ 
doc            └─────────────────┘      └─────────────────┘  └────────┘
753  { add_le_add_left := λ a b h c, @add_le_add_left' α _ b a c h,
id                                └──────────────┘       
src                                   └──────────────┘
typ                               └──────────────┘       
754    lt_of_add_lt_add_left := λ a b c h, @lt_of_add_lt_add_left' α _ a c b h,
id                                      └────────────────────┘       
src                                         └────────────────────┘
typ                                     └────────────────────┘       
755    ..order_dual.partial_order α,
id       └──────────────────────┘ 
src      └──────────────────────┘
typ      └──────────────────────┘ 
756    ..show add_comm_monoid α, by apply_instance }
id            └─────────────┘ 
src           └─────────────┘       └─────────────┘
typ           └─────────────┘      └─────────────┘
doc                                 └─────────────┘
txt                                 └─────────────┘
par                                 └─────────────┘
pid                                               
st                                 └──────────────┘
757  
758  instance [ordered_cancel_comm_monoid α] : ordered_cancel_comm_monoid (order_dual α) :=
id             └────────────────────────┘     └────────────────────────┘  └────────┘ 
src            └────────────────────────┘      └────────────────────────┘  └────────┘
typ            └────────────────────────┘     └────────────────────────┘  └────────┘ 
doc                                                                        └────────┘
759  { le_of_add_le_add_left := λ a b c : α, le_of_add_le_add_left,
id                                          └───────────────────┘
src                                          └───────────────────┘
typ                                         └───────────────────┘
760    add_left_cancel := @add_left_cancel α _,
id                         └─────────────┘ 
src                        └─────────────┘
typ                        └─────────────┘ 
761    add_right_cancel := @add_right_cancel α _,
id                          └──────────────┘ 
src                         └──────────────┘
typ                         └──────────────┘ 
762    ..order_dual.ordered_comm_monoid }
id       └────────────────────────────┘
src      └────────────────────────────┘
typ      └────────────────────────────┘
763  
764  instance [ordered_comm_group α] : ordered_comm_group (order_dual α) :=
id             └────────────────┘     └────────────────┘  └────────┘ 
src            └────────────────┘      └────────────────┘  └────────┘
typ            └────────────────┘     └────────────────┘  └────────┘ 
doc                                                        └────────┘
765  { add_lt_add_left := λ a b : α, ordered_comm_group.add_lt_add_left b a,
id                                  └────────────────────────────────┘  
src                                  └────────────────────────────────┘
typ                                 └────────────────────────────────┘  
766    add_left_neg := λ a : α, add_left_neg a,
id                             └──────────┘ 
src                             └──────────┘
typ                            └──────────┘ 
767    ..order_dual.ordered_comm_monoid,
id       └────────────────────────────┘
src      └────────────────────────────┘
typ      └────────────────────────────┘
768    ..show add_comm_group α, by apply_instance }
id            └────────────┘ 
src           └────────────┘       └─────────────┘
typ           └────────────┘      └─────────────┘
doc                                └─────────────┘
txt                                └─────────────┘
par                                └─────────────┘
pid                                              
st                                └──────────────┘
769  
770  end order_dual